4 ms·
If you just care about the correctness of some algorithm, proving it is just tedium and not likely to produce a proof useful for reading anyway. So an exception
by roywiggins 9y ago
If you just care about the correctness of some algorithm, proving it is just tedium and not likely to produce a proof useful for reading anyway. So an exceptionally long, boring proof of correctness generated by a supercomputer is perfectly fine.
- nickpsecurity 9y agoThis 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.