News for hackers. Stuff that matters.
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.
Re:The Case for Formal Verification (2013) by CHY872 on Monday April 21, 2014 @12:34PM (#7621923)
My first opportunity to whip this one out :) https://cakeml.org/popl14.pdf
Re:The Case for Formal Verification (2013) by munin on Monday April 21, 2014 @01:02PM (#7622114)
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/.