See also CakeML, "A verified implementation of a significant subset of Standard ML in the HOL4 theorem prover". https://cakeml.org/ https://cakeml.org/ Not th

See also CakeML, "A verified implementation of a significant subset of Standard ML in the HOL4 theorem prover". https://cakeml.org/ https://cakeml.org/ Not that this project, unlike CompCert, is Free Software in the Stallman sense: https://github.com/CakeML/cakeml/blob/master/COPYING https://github.com/CakeML/cakeml/blob/master/COPYING