New year, new Advent of Code. I like to use it to provide momentum to learn something new about programming. I think there’s a lot to be said for experimenting with different ways to write the same (class of) programs. Last year I did Prolog and learned about constraint logic programming. This year I’ve been using Lean 4, and trying to learn more about program verification and dependently typed programming.
It’s already been a fun learning experience, and I thought I’d note down some stuff I learned that wasn’t immediately obvious from the popular learning materials like the official lean books (Programming in Lean and Theorem Proving in Lean 4).
Say you have a function foo, and you want to make sure foo 2 = 5. Well, in lean you can start off with this:
def foo (x : Nat) := sorry
#eval foo 2Now, you have foo defined, and you’ll get live updates in the infoview on the output as you edit the file.
Once you’re done being sorry, you can replace #eval with #guard, which takes a boolean and does nothing if it’s true and a compile error otherwise:
#guard foo 2 = 5If you like snapshot testing, that’s also built-in:
/--
info: 5
-/
#guard_msgs in
#eval foo 2This will print a diff to the infoview whenever the stdout from #eval isn’t equal to the docstring above, and nothing otherwise.
As a longtime lisper, this workflow in some ways feels even more interactive than what you get with a traditional REPL, even nice ones like in Common Lisp (though obviously there are other things that aren’t there).
One thing to note is that you can run IO actions in #eval, and that they reevaluate in an unpredictable way. Sometimes I had to do spurious edits to a #eval line to deal with a stale evaluation in the infoview. As such, you probably don’t want to run nontrivial IO actions in #eval (printing to stdout is fine).
You can write code with local mutable variables anywhere pretty easily. Lean’s support for do-notation comes with local mutable variables out of the box. It also gives you for loops.
All you have to do to get access to these features is enter the Identity monad using Id.run. Here’s what it looks like in practice:
def part1_solve (input: List Int) : Nat := Id.run do
let mut count : Nat := 0
let mut pos : {x : Int // 0 ≤ x ∧ x < 100} := ⟨50, by omega⟩
for op in input do
pos := ⟨(pos + op) % 100, by omega⟩
if pos.val == 0 then
count := count + 1
return countdef dbgTrace {α : Type u} (s : String) (f : Unit → α) : αIt prints s, and then calls f on the unit value and returns that.
One thing to note is that the compiler will absolutely throw away your dbgTrace expressions if they look like dead code (i.e you must use the return value). Debug printing itself is not considered a side-effect as far as the compiler is concerned (Lean is a referentially transparent language).
More convenient is dbgTraceVal:
def dbgTraceVal {α : Type u} [ToString α] (a : α) : αIt’s the identity function except it also debug prints its argument.
Good printf debugging means custom format strings. Lean has those too! You can access the lean equivalent of python-style f-strings with the s! sigil. It looks like this:
dbgTrace s!"woah: {expr1}" (fun () => expr2)Note that unlike say Rust, you can write expressions in the template strings, not just variable names.
There’s also m! and f! which produce different forms of structured data instead of strings which I won’t get into. You can define your own sigils too, f! is a macro defined in the stdlib.
Lean has the full gamut of assertions, and it also has easy access to automatic theorem proving as well as interactive theorem proving.
It has assert! and debug_assert! which do what you expect. But you can go further with refinement types. Those look like {x : T // P(x)} which is a type that contains a term of type T as well as a proof that the predicate P holds on it. You can construct them with the syntax ⟨value, proof_term⟩. This is just a regular struct under the hood, with two fields .val and .property which are what you expect.
The cool bit is that you can use many kinds of proof automation (i.e tactics) to construct the proofs, which can make it very lightweight. If you see my simple example from earlier, you can see that the proof term I had to construct was just by omega, because the omega tactic is strong enough to construct the proof on its own!
More and smarter tactics is an active area of development.
I think it’s pretty cool that you can write a normal program and then increase the level of assurance using verification in a gradual way like this.
Being forced to use VSCode, as silly as it sounds, has put me off playing with Lean before. As it happens, it’s actually really easy to use Emacs (and supposedly vim, but I wouldn’t know).
I just added this to my emacs config (I use use-package with straight.el):
(use-package lean4-mode
:commands lean4-mode
:mode "\\.lean\\'"
:straight (lean4-mode :type git :host github
:repo "leanprover-community/lean4-mode"
:files ("*.el" "data")))Note that lean4-mode is integrated with lsp-mode which is nonnegotiable. I normally use eglot as my lsp-client so now I have both installed which is stinky IMO but eh I can deal with it. It’s also hardcoded to use company-mode, and I had to locally disable corfu-mode in lean4 buffers or it would automatically hang every once in a while.
Putting those nits aside, the experience is pretty good. The only thing you need other than the mode is to have lean in your path.
elanTo have lean in your path the thing you have to use is elan which is lean’s toolchain manager (like rustup, ghcup, etc). It downloads lean toolchain binaries (i.e lean itself, the build tool lake, etc) to ~/.elan/ and puts them in your path. elan itself is available on nixpkgs so I could grab it with a nix shell nixpkgs#elan.
These days I like to have all my software projects be at least somewhat reproducible using a nix flake devshell, so I would prefer to have my toolchain version pinned and managed by nix. Also I don’t like “download random binary” to be part of my workflow.
Lean 4 removed their user-facing nix flake a while back though, because they didn’t want to maintain it. But, a brave soul has created lean4-nix which provides an overlay for nix toolchains. This works for me.
The caveat here is that it seems that without an elan in the path, lake refuses to create or update lake-manifest.json (basically the package lockfile), which becomes necessary if you want to use dependencies.
Lean is pretty cool. I’ve been having a lot of fun exploring it and I think the trend towards more ergonomic program verification is the future of software.
Also Stanford CS ⑨⑨ - Perfect Math Class is a great resource to learn from.