3 ms·
> And C is also AFAIK the only language with a formally proven compiler CompCert C. There's CakeML, which is a formally verified subset of Standard ML [0] [0]
by aw1621107 4y ago
> And C is also AFAIK the only language with a formally proven compiler CompCert C.
There's CakeML, which is a formally verified subset of Standard ML [0]
[0]: https://cakeml.org/popl14.pdf https://cakeml.org/popl14.pdf