11 ms·
From the paper you can see that they actually target CompCertTSO (a C subset) https://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/ https://www.cl.cam.ac.uk/~pes20/
by twoWhlsGud 6y ago
From the paper you can see that they actually target CompCertTSO (a C subset)
https://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/ https://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/
from the CompCert folks - who do formally verified C compilers (also worth looking at, btw). Targeting a subset of C allows them to preserve their behavioral guarantees in way that would be challenging I think with the full C language. So it's not an unreasonable subset to pick if you're serious about predictable outcomes.
- MaxBarraclough 6y agoThanks. I read Via a C-like language to mean their language compiles to a non-standard language resembling C, but as you say, they mean they defined a novel language that resembles C, and it compiles down to standard C (specifically, the C subset named ClightTSO suitable for use with the CompCertTSO compiler). Nowhere in Armada's overview [0] is it stated that the ultimate goal is to produce verified C code. I've heard of CompCert. Pity it hasn't got more traction. Also a pity about its licensing situation. The Free and Open Source community is not interested in semi-Free software. The DMD compiler showed us this. [0] https://github.com/microsoft/Armada https://github.com/microsoft/Armada
- MaxBarraclough 6y agoUpdate: I created a GitHub Issue to point out the omission. The overview has now been clarified.