[kmill]

Leo de Moura wants Lean 4 to be used for software verification too.

A cool thing about Lean 4 is that it's also a programming language, using the same syntax as for proofs, making it easy to consider proving correctness properties of programs you write. Most of Lean 4 and its tactics are written in Lean 4 (though at this point almost none of this code has any associated proofs).

[dunham]

Yeah, I believe they said they intend for it to be used as a general purpose programming language. I used it to complete Advent of Code last year.

There are some really interesting features for general purpose programming in there. For example: you can code updates to arrays in a functional style (change a value, get a new array back), but if the refcount is 1, it updates in place. This works for inductive types and structures, too. So I was able to efficiently use C-style arrays (O(1) update/lookup) while writing functional code. (paper: https://arxiv.org/abs/1908.05647 )

Another interesting feature is that the "do" blocks include mutable variables and for loops (with continue / break / return), that gets compiled down to monad operations. (paper: https://dl.acm.org/doi/10.1145/3547640 )

And I'm impressed that you can add to the syntax of the language, in the same way that the language is implemented, and then use that syntax in the next line of code. (paper: https://lmcs.episciences.org/9362/pdf ). There is an example in the source repository that adds and then uses a JSX-like syntax. (https://github.com/leanprover/lean4/blob/master/tests/playgr... )

[pjmlp]

Yeah, here is where TLA+ fails to gain adoption, because it is only a model, how people actually implement the architecture is completely unrelated to how the model was validated.

[nextaccountic]

> Most of Lean 4 and its tactics are written in Lean 4 (though at this point almost none of this code has any associated proofs).

Do you have to actually prove a tactic work for it to be sound? A tactic will rewrite the program into a simplified program that will verified by a kernel; if the tactic wrongly expands something, the kernel will later reject the program. Only the itself kernel need to be verified for the whole thing to be sound.

Or am I missing something?

[kmill]

You're not missing anything. I was going to mention this but decided not to get into it. (One detail: you can't verify the kernel exactly because of Gödel incompleteness issues.)