Re:The Case for Formal Verification (2013)
by munin on Monday April 21, 2014 @10:17AM
(#7621131)
friends of mine have still segfaulted mlton-compiled SML programs. as I understand it, you need to have a bisimulation-based proof that shows equivalence in states between ML and x86, and as far as I know that just hasn't been done. until then you have the risk of a bug in some aspect of the compiler, which has happened, emitting code that produces a crash or something else bad.
[ Parent
| on HN ]
My first opportunity to whip this one out :) https://cakeml.org/popl14.pdf
nice!
Re:The Case for Formal Verification (2013)
by vilhelm_s on Monday April 21, 2014 @12:53PM
(#7622038)
It has been done: https://cakeml.org/.