Warning! Lots of disjointed thoughts below.<p>I've used Frama-C ACSL+WP and it was incredibly painful to use to prove basically anything.<p>For me the main issue was that Frama-C can say 3 things about your specs: Yes, No, and Don't know. That means I have no idea where to start to debug my proof, especially as I'm already convinced that my proof works! This is inherent to computing weakest pre-condition AFAIK. I had to provide my own loop invariants, which is also a pain :-).<p>C's semantics also makes a lot of things which I would assume was "trivially true" fail verification. This isn't Frama-C's fault however, of course.<p>I haven't used the other plugins, perhaps there are better ones!<p>Type systems can be quite nice with regards to error messages, especially as the programmer themselves essentially derive their own granularity with regards to the domain and the proofs of the domain. But yes, we all have examples of absolutely terrible type system error messages.<p>The paradigm of making comments have semantic meaning in some other language is also terrible. I'd rather have a superset of the core language with syntactic extensions for proofs. The build system can pull out the core language source code for me.<p>Finally:<p>I think that abstract interpretation of a low-level compilation target combined with a proof-carrying compiler is the way to go. The compiler has proofs of a bunch of stuff regarding the code already, carry them down into the assembly level please! There's some work in abstract interpretation of WebAssembly, and I think that could be a great platform for formal verification.<p>Sorry for the barfing :-). Hopefully there're thoughts here to react to and reply to me about!
I'm starting my PhD under the supervision of one of the Frama-C authors, if you have questions I can relay them.<p>In general I've found deductive verification techniques interesting / promising because they free engineers of a lot of required but tedious details you'd have in ITPs.<p>However, I think there's a LOT of room for improvement in terms of ergonomics of proof debugging. For a frequent (for me) problem when debugging invariants is conditionals that break the invariant.<p>if i have some code doing something like<p><pre><code> while (X) {
invariant { forall i. 0 <= i < N .... }
if j < i A else B
}
</code></pre>
But it turns out that one of the branches A, B doesn't preserve the invariant well all the provers will tell me is 'can't prove this!' it's up to you to perform the transformations that split the two cases (granted in this example it's trivial) so that you can see that only _one_ branch was failing.<p>I think that there should be transforms that automatically do things like split the range of an interval along relevant points (aka j) to help you figure out which portions are failing.<p>There are tons of other issues related to proof ergonomics that could be improved, the UIs are really stuck in the 90s!
Since you mentioned it, some posts I wrote a while back about Frama-C:<p>Applied Formal Logic: Brute Force String Search <a href="https://maniagnosis.crsr.net/2017/06/AFL-brute-force-search.html" rel="nofollow">https://maniagnosis.crsr.net/2017/06/AFL-brute-force-search....</a><p>Applied Formal Logic: The bug in Quick Search. <a href="https://maniagnosis.crsr.net/2017/06/AFL-bug-in-quicksearch.html" rel="nofollow">https://maniagnosis.crsr.net/2017/06/AFL-bug-in-quicksearch....</a><p>Applied Formal Logic: Correctness of Quick Search. <a href="https://maniagnosis.crsr.net/2017/07/AFL-correctness-of-quicksearch.html" rel="nofollow">https://maniagnosis.crsr.net/2017/07/AFL-correctness-of-quic...</a>
A few years ago, I learnt of one of the surprising constraints for Frama-C: it may only depend on code that could be patched by the maintainers of Frama-C.<p>That's because Frama-C is meant to be used on highly critical infrastructures (think nuclear plants) even in highly difficult times (think world war).
We should be spending a lot less time inventing new languages and spending a lot more time working on tools for existing languages. If we did, all languages would be better, and the languages we did design would be designed to make it easy to make tools that help us use them.