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
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.
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/.
Does Safe Haskell guatantee enough, or do we need more?
that is not true, you need much stronger guarantees than just typechecking gives you. you also have a large wodge of native code for the runtime that is not written in the strongly typed language.