Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

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!


It has been done: https://cakeml.org/.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: