What even is the most complex programming language with a fully machine-checkable spec? Are there actually practically useful ones? I know of none.
What even is the most complex programming language with a fully machine-checkable spec? Are there actually practically useful ones? I know of none.
One candidate is ATS [1].
Another, https://cakeml.org/
[1]: https://en.wikipedia.org/wiki/ATS_(programming_language)
For 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!
There'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.