5 ms·
Neither the Rust nor the Ada spec is formal, in the sense of consumable by a theorem prover. AFAIK for Ada Spark, there is of course assumptions on the language
by wucke13 1y ago
Neither the Rust nor the Ada spec is formal, in the sense of consumable by a theorem prover. AFAIK for Ada Spark, there is of course assumptions on the language semantics built-in to Spark, but: these are nowhere coherently written down in a truly formal (as in machine-readable) spec.
- Sharlin 1y agoWhat 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!
- shakna 1y agoThere was also Larch/Ada [0], which was a formally proved subset of Ada, developed for NASA [1]. [0] https://apps.dtic.mil/sti/tr/pdf/ADA249418.pdf https://apps.dtic.mil/sti/tr/pdf/ADA249418.pdf [1] https://ntrs.nasa.gov/citations/19960000030 https://ntrs.nasa.gov/citations/19960000030