Heh, seems this is the third time this has been posted. I wonder how much real world use it’s gotten?
I love the idea of being able to program this way, in sensitive regions of the code. I’m less thrilled by using an entirely different language to do it, esp. one with some odd syntactic quirks like resurrecting Pascal’s <> operator instead of !=.
I’d love to see these features added as extensions to C/++, like specifying a valid range for an integer variable so a static analyzer and/or undefined-behavior sanitizer can use that knowledge. I think Clang already has some of these, like “facts that guarantee a condition is true. Better support for pre and postconditions would be great.
frama-C already supports this via the wp plugin. You can prove sections of code free from overflow.
A good tutorial: https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf