This sort of thing is standard in Frama-C and SPARK Ada for proving code to be safe from common vulnerabilities or crashes. I don't care what the proof terms lo

This sort of thing is standard in Frama-C and SPARK Ada for proving code to be safe from common vulnerabilities or crashes. I don't care what the proof terms look like: just that the code won't get hacked. Same with CompCert even though it's meant to be readable. I just want a correct compilation. Lots of situations where the result obtained is only thing that matters to most users.