3 ms·

Perhaps worth noting is Armada https://github.com/microsoft/Armada https://github.com/microsoft/Armada which is built upon Dafny and targets a C-like language

Perhaps worth noting is Armada https://github.com/microsoft/Armada https://github.com/microsoft/Armada which is built upon Dafny and targets a C-like language.

MaxBarraclough 6y ago
Thanks, I hadn't heard of that project. Their paper is at [0] (which I've only skimmed terribly quickly). I'm not quite sure what to make of 'targets a C-like language'. Does that mean, put bluntly, that it's not practical? Can it be made to target standard C? While we're here, a shoutout to ZZ / ZetZ, [1] which we discussed 5 months ago at [2]. It's a verifiable C-style language which compiles down to standard C. I'm not sure how mature the language is at this point. (It still pains me that my prominent comment at [2] turned out to be fundamentally mistaken.) And let's finish up the tour with a quick mention of Frama-C [3] and the (sadly proprietary) Escher C Verifier, [4] both of which work with C directly. [0] https://jamesrwilcox.com/armada.pdf https://jamesrwilcox.com/armada.pdf [1] https://github.com/zetzit/zz https://github.com/zetzit/zz [2] https://news.ycombinator.com/item?id=22245409 https://news.ycombinator.com/item?id=22245409 [3] http://frama-c.com/acsl_tutorial_index.html http://frama-c.com/acsl_tutorial_index.html [4] https://www.eschertech.com/products/ecv.php https://www.eschertech.com/products/ecv.php
- 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 ago
    Thanks. 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 ago
    Update: I created a GitHub Issue to point out the omission. The overview has now been clarified.

Perhaps worth noting is Armada https://github.com/microsoft/Armada https://github.com/microsoft/Armada which is built upon Dafny and targets a C-like language.

MaxBarraclough 6y ago

Thanks, I hadn't heard of that project. Their paper is at [0] (which I've only skimmed terribly quickly). I'm not quite sure what to make of 'targets a C-like language'. Does that mean, put bluntly, that it's not practical? Can it be made to target standard C? While we're here, a shoutout to ZZ / ZetZ, [1] which we discussed 5 months ago at [2]. It's a verifiable C-style language which compiles down to standard C. I'm not sure how mature the language is at this point. (It still pains me that my prominent comment at [2] turned out to be fundamentally mistaken.) And let's finish up the tour with a quick mention of Frama-C [3] and the (sadly proprietary) Escher C Verifier, [4] both of which work with C directly. [0] https://jamesrwilcox.com/armada.pdf https://jamesrwilcox.com/armada.pdf [1] https://github.com/zetzit/zz https://github.com/zetzit/zz [2] https://news.ycombinator.com/item?id=22245409 https://news.ycombinator.com/item?id=22245409 [3] http://frama-c.com/acsl_tutorial_index.html http://frama-c.com/acsl_tutorial_index.html [4] https://www.eschertech.com/products/ecv.php https://www.eschertech.com/products/ecv.php

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 ago
  Thanks. 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 ago
  Update: I created a GitHub Issue to point out the omission. The overview has now been clarified.