4 ms·
What even is the most complex programming language with a fully machine-checkable spec? Are there actually practically useful ones? I know of none.
by Sharlin 1y ago
What even is the most complex programming language with a fully machine-checkable spec? Are there actually practically useful ones? I know of none.
- nine_k 1y agoOne candidate is ATS [1]. Another, https://cakeml.org/ https://cakeml.org/ [1]: https://en.wikipedia.org/wiki/ATS_(programming_language) https://en.wikipedia.org/wiki/ATS_(programming_language)
- gpm 1y agoThere's a formally verified C compiler, IIRC the frontend isn't, but if you define the language to the structs that are in the inputs to whatever is formally verified I guess whatever C like dialect of a language it implements must be.
- wucke13 1y agoFor the seL4 proofs a subset of C was formalized, for example. (Already mentioned) CakeML would be another example, together maybe with its Pancake sibling. Also: WebAssembly!