3 ms·
And C is also AFAIK the only language with a formally proven compiler CompCert C. If you used something else, you'd need to trust a lot more code.
by renox 4y ago
And C is also AFAIK the only language with a formally proven compiler CompCert C.
If you used something else, you'd need to trust a lot more code.
- vore 4y agoCompCert doesn't stop you from writing memory unsafe C, of course, just that it won't miscompile your maybe memory unsafe C.
- 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
- kobebrookskC3 4y agocuriously, seL4 doesn't need to trust the compiler: the assembly is verified to satisfy the abstract specification