5 ms·
> if a program compiles one can know that it will never crash that is not true, you need much stronger guarantees than just typechecking gives you. you also ha
by munin 13y ago
> if a program compiles one can know that it will never crash
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.
- sanxiyn 13y agoDoes Safe Haskell guatantee enough, or do we need more?
- munin 13y agoI don't think so, there have been bugs in ghc before, the problem would be a bug in ghc that emits code that crashes.
- CHY872 13y agoOk, 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.