3 ms·

If/when Lean 4 matures more and adds support for formal verification of code, I would like to see it gain high-quality fuzzers as well. Its relatively good spe

If/when Lean 4 matures more and adds support for formal verification of code, I would like to see it gain high-quality fuzzers as well. Its relatively good speed (hopefully with the new compiler) could make it a good candidate for fusing these two strategies.

aSanchezStern 3y ago
Uhhhh, I'm pretty sure Lean already allows for formal verification of code. In the meta theory that tools like Lean and Coq operate, proofs and programs are very intertwined; it's not really possible to build a proving system in this metatheory without also allowing for program verification. Maybe you're talking about gaining support for formal verification of code not written in Lean? Like, being able to verify C? In that case, it's actually just a library issue. Nothing needs to be changed about the core Lean language, someone just needs to formalize the semantics of the target language semantics in Lean, and then add a verified compiler and verified extraction if you want to make the guarantees extend directly to the compiled assembly. Fuzzers have actually combined well with theorem proving in these kinds of tools in the past; Coq, the proof assistant that heavily inspired Lean and has been in constant use since the mid 80's, has a library QuickChick (based on QuickCheck from the Haskell world) which takes an arbitrary property and generates test inputs to test it, and has very mature support for extending it with new datatypes and invariants.
- ykonstant 3y ago
  Lean allows formal verification, but it does not make it easy. As staunton remarked, the devs are focusing on classical mathematics, and the ergonomics for verifying code are currently horrible. I do suspect this will change with time, though.
staunton 3y ago
Why do you name Lean here as opposed to the other provers? Lean is "the new shiny thing" but my impression is that the community sees its focus in math, not so much software verification. Quite a few design decisions (e.g. focus on classical reasoning support, focus of existing libraries) suggest that software verification of Lean programs isn't seen as a major application. (Of course you can always define a framework and prove stuff about C programs, like the "software foundations" book illustrates in Coq. But that's not really something new and again would need a lot of foundational work and tooling, essentially duplicating what people do with Coq, for no obvious benefit).
- ykonstant 3y ago
  That's because it's the one I know and am using. I agree the devs are focusing on classical mathematics, but given Lean's dual purpose as a general-purpose programming language, one can imagine a workflow of writing Lean code and verifying it in the language. It's up to the community if they want to do this.

aSanchezStern 3y ago

Uhhhh, I'm pretty sure Lean already allows for formal verification of code. In the meta theory that tools like Lean and Coq operate, proofs and programs are very intertwined; it's not really possible to build a proving system in this metatheory without also allowing for program verification. Maybe you're talking about gaining support for formal verification of code not written in Lean? Like, being able to verify C? In that case, it's actually just a library issue. Nothing needs to be changed about the core Lean language, someone just needs to formalize the semantics of the target language semantics in Lean, and then add a verified compiler and verified extraction if you want to make the guarantees extend directly to the compiled assembly. Fuzzers have actually combined well with theorem proving in these kinds of tools in the past; Coq, the proof assistant that heavily inspired Lean and has been in constant use since the mid 80's, has a library QuickChick (based on QuickCheck from the Haskell world) which takes an arbitrary property and generates test inputs to test it, and has very mature support for extending it with new datatypes and invariants.

ykonstant 3y ago
Lean allows formal verification, but it does not make it easy. As staunton remarked, the devs are focusing on classical mathematics, and the ergonomics for verifying code are currently horrible. I do suspect this will change with time, though.

staunton 3y ago

Why do you name Lean here as opposed to the other provers? Lean is "the new shiny thing" but my impression is that the community sees its focus in math, not so much software verification. Quite a few design decisions (e.g. focus on classical reasoning support, focus of existing libraries) suggest that software verification of Lean programs isn't seen as a major application. (Of course you can always define a framework and prove stuff about C programs, like the "software foundations" book illustrates in Coq. But that's not really something new and again would need a lot of foundational work and tooling, essentially duplicating what people do with Coq, for no obvious benefit).

ykonstant 3y ago
That's because it's the one I know and am using. I agree the devs are focusing on classical mathematics, but given Lean's dual purpose as a general-purpose programming language, one can imagine a workflow of writing Lean code and verifying it in the language. It's up to the community if they want to do this.