Formally Verifying the Easy Part

Formally Verifying the Easy Part(brainflow.substack.com)

3 points by hnipps 101 days ago | 5 comments

derrak 101 days ago |

> The proofs stop at the language boundary. The bugs don’t.

In formal verification, you have to model everything you care about. I suspect we’ll see large fragments of popular languages being more thoroughly modeled in languages like Dafny and Lean.

An alternative that side steps all of this is to not use an external language at all. ACL2 might be a better fit in this regime than Dafny or Lean because of how close it sits to SBCL.

hnipps 101 days ago | |

I suspect the same but I wonder how effective it will be in reality. I mention a group that has been trying to verify SQL for 12 years, and they haven't fully formalised all basic queries.

I think LLMs will speed things up but will it result in popular libraries becoming verified or an entirely new class of libraries being built and verified from the ground up?

ACL2 sounds interesting. Do you use it?

derrak 101 days ago | | |

I do use ACL2, although I don’t do many proofs. When I do, the proofs usually go through automatically or require me to state only a few lemmas or tell the tool how to do the induction.

This is partially a commentary on how good the automation is in ACL2 and partially a commentary on the fact that I don’t use it for hard problems :)

I use it more for property based testing. The counterexample generator is very powerful because it leverages the knowledge base of the theorem prover (all the accumulated lemmas, etc.) among other things.