4 ms·
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
by CHY872 13y ago
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 http://www.cl.cam.ac.uk/teaching/1314/FoundsCS/fcs-notes.pdf
[2] http://gallium.inria.fr/~fpottier/publis/fpottier-regis-gianas-typed-lr.pdf http://gallium.inria.fr/~fpottier/publis/fpottier-regis-gian...
[3] https://en.wikipedia.org/wiki/Type_safety#Standard_ML https://en.wikipedia.org/wiki/Type_safety#Standard_ML
- munin 13y agofriends 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.