Is the experience here much different from Idris? The latter was more a language that can also be used for proofs, whereas Lean came out of a proof assistant. Does that lead to much difference in use, or do the approaches essentially converge?
Looking briefly at the example code, it seems pretty similar.
I did advent of code in Lean4 in 2022 and Idris2 in 2021. Lean4 was fairly similar to Idris code-wise.
Minor differences:
- On the Lean side I leveraged the fact that Arrays can mutate in place (if the refcount is 1). For Idris I'd use a Buffer (IO Monad) or SortedMap.
- Lean has a nice mechanism where I can drop an #eval or #check in the code and have the result show up in an editor pane. For most days, I never compiled/ran the code separately.
- Lean defaults to total, so I had to put partial in a couple of places.[1]
- Lean could have accepted proofs that my indices were in range, but I used the unsafe functions instead.[2]
- Idris has some nice editor functionality to stub out functions and case splits for you.
[1]: Idris2 defaults to "covering", which says case splits have to cover, but relaxes termination checking. A couple of the spots where I put partial in lean could be proven total, but I was not familiar with the theorem proving corner of lean. Idris totality checking is slightly different in that you can't add proofs, but I think you can achieve the same results by adding additional arguments.
[2]: Because I didn't know the theorem proving bits, but I intend to go back and try to patch these up as an exercise.
I think they end up similar. Although Lean 3 is much more geared towards writing proofs with the addition of mathlib [0] which aims to be a library of formalized mathematics.
Looking briefly at the example code, it seems pretty similar.