> 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.
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.