The Case for Formal Verification (2013)

Re:The Case for Formal Verification (2013) by CHY872 on Monday April 21, 2014 @04:51AM (#7620320)

Ok, so in retrospect I didn't mean that for OCaml. Certainly it is true for Standard ML [1, 2, 3], or rather, the parts of the language that use the underlying native code (IO etc) are generally smaller pieces of code for which the correctness properties are hopefully more easily tested and verified. In any case, I believe my point still stands on the whole :)

[1] http://www.cl.cam.ac.uk/teaching/1314/FoundsCS/fcs-notes.pdf [2] http://gallium.inria.fr/~fpottier/publis/fpottier-regis-gian... [3] https://en.wikipedia.org/wiki/Type_safety#Standard_ML

[ Parent | on HN ]

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 ]

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

[ Parent | on HN ]

Re:The Case for Formal Verification (2013) by munin on Monday April 21, 2014 @01:02PM (#7622114)

nice!

[ Parent | on HN ]

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/.

[ Parent | on HN ]