How does Perfect Developer compare to Frama-C? Is it more capable or maybe simply more convenient for MISRA verification?
For the unfamiliar, see http://frama-c.com/ and https://en.wikipedia.org/wiki/Frama-C
For the unfamiliar, see http://frama-c.com/ and https://en.wikipedia.org/wiki/Frama-C
Curiously it involves Haskell for its specification. [0]
They've also done some very impressive work verifying that the ARM machine code corresponds to the verified C code. They did this not by using a formally verified compiler, but by using GCC and then verifying the correspondence afterwards.
> Is it possible to have a programming language where the compiler does the formal verification?
Yes, but these languages are not all that approachable.
There's SPARK, which is Ada-based and has seen real-world use in various life-or-death applications like military aviation.
There's also ZZ, which is in early days, and which aims to be closer to C. [2] [3]
There's also Perfect Developer, a proprietary payware product, which does impressive things adding formal verification machinery to C and C++. [4]
[0] https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass...
[1] https://en.wikipedia.org/wiki/SPARK_(programming_language)
[2] https://github.com/aep/zz
[3] https://news.ycombinator.com/item?id=22245409
[4] https://www.eschertech.com/articles/index.php