Comment by solomonb
2 days ago
The secret of Lean4 is that its actually a great programming language, sort like a super Haskell. In fact I like it more as a programming language then as a proof checker!
Dependent types are awesome for regular programming in addition to formal verification. For proof checking I actually prefer Agda.
Any experience with Rocq? I've been curious about jumping into dependent types.
I've never used Rocq but from what I understand the core type theory is also a version of CIC and like Lean it has strong support for tactics. Rocq defaults to an axiom free core making it constructive. Classical axioms like propositional extensionality and axiom of choice are things you opt into deliberately.
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.
> The secret of Lean4 is that its actually a great programming language
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.
I would consider using it on any greenfield personal project where I would ordinarily use Haskell.
another one that seems practical, but I never tried, is F* (Fstar)