|
|
|
|
|
|
by touisteur
1945 days ago
|
|
|
I think there's already an industrial-grade middleground that is used by at least 2 major automated and interactive proof environments: Why3. Spark and Frama-C use it and it seems part of their success is from it and the ability to use all the SMT engines that Why3 talks to, and also there are bridges to Coq and Isabelle. I've seen people use 'em! Sadly most of us don't get to rewrite or greenfield stuff, and although Spark is designed to be very progressive and modular, the proof of code that wasn't "written with proof in mind" is still quite the effort. |
|
|