> And C is also AFAIK the only language with a formally proven compiler CompCert... | Hacker News

Hacker News new | past | comments | ask | show | jobs | submit

login

aw1621107 on Feb 5, 2023 | parent | context | favorite | on: I use C when I believe in memory safety

> 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

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