3 ms·
Could someone familiar with Verus comment on the power and expressiveness of Verus vs. Lean4 I understand Verus is an SMT based verification tool, and Lean is
by camkego 2y ago
Could someone familiar with Verus comment on the power and expressiveness of Verus vs. Lean4
I understand Verus is an SMT based verification tool, and Lean is both an interactive prover and SMT based tool.
But my understanding in the area of formal verification is limited, and it would be good to get an opinion from someone well versed in formal methods for software.
- staunton 2y agoLean is similar to Coq. You could - state and prove things about (e.g.) C code, like the "Software Foundations" book does for Coq. However, nobody seems to be doing this with Lean and the tools are missing. - write programs in Lean4 and prove things about them. Some people are doing this a tiny little bit. - formalize pure math and publish papers about that. This is what Lean4 (and Coq) is mostly used for. The kinds of things Lean/Coq are able to practically state and prove are more general. Maybe you don't need that generality for real-world programs though.