I built the RealWorld app in Lean 4
leangineer.com
leangineer.com
Dependent types are awesome for regular programming in addition to formal verification. For proof checking I actually prefer Agda.
From what I understand the Lean community leans (haha) classical and uses these axioms throughout mathlib. By staying constructive you guarantee that closed proofs can, in principle, evaluate to a canonical form.
Kind of feels like you have to specify for what here, as no programming language is just "great at everything", they all have their places (except Clojure and children which is great at everything obviously). Say I run shell commands, obviously a PL based around proofs will be way too much, compared to if I want to create aircraft stabilizer with movable control surfaces.
However, after some consideration I opted to not move forward with it just yet. The problem is that at least for that particular case I could only really practically prove some properties of the code. With more time I could perhaps bring it up further. So for entirely practical reasons I am still going to want tests for the rest of the code. And while Idris 2 does have support for testing and continuous integration, at that time there were no solutions for measuring test coverage or performing mutation testing.
It does seem like since then someone has created a coverage tool for Idris 2, but mutation testing tooling still doesn't exist.
Lean 4 doesn't seem to have anything for coverage yet. I found some tool that claims to do a kind of mutation testing for Lean 4, but it sounds like it is still quite narrow in what it supports.
OTOH, my borrow checker is provably sound, which is why I am using it.
You can have one piece of software that does things, and a separate piece that proves that the things the first piece does are correct.
This is an implementation choice you did when implementing your programming language, if I understand correctly.
I thought of it because writing some lean lang I also had the option of adding Mathlib or keep it "bare".