7 ms·

I've only ever watched SPARK Ada from afar and never written code using it, so keep in mind that my comment might be a bit one-sided. I doubt Dafny will have n

I've only ever watched SPARK Ada from afar and never written code using it, so keep in mind that my comment might be a bit one-sided. I doubt Dafny will have native targets (which I assume is a prerequisite for the "critical-systems" work you're talking about) any time soon if ever. There's just not enough resources behind it. AFAICT, basically all the development, Stack Overflow answering, etc. is all powered by a single dude (Rustan Leino). So I don't think it'll be competing in the same space as SPARK Ada any time soon simply due to resource availability. Nonetheless Dafny as a language is, I think, strictly more expressive than SPARK. For example, Dafny's functions (vs methods) allow for the very nice expression of arithmetic invariants that I don't think SPARK supports (look at the Fibonacci example in the online tutorial here: https://rise4fun.com/Dafny/tutorial https://rise4fun.com/Dafny/tutorial that has the standard mathematical definition of Fibonacci numbers as a function and then implements it as a method).

MaxBarraclough 6y ago
> I doubt Dafny will have native targets (which I assume is a prerequisite for the "critical-systems" work you're talking about) any time soon if ever Fair enough. Still a really neat project. I forgot to ask an obvious question: Dafny uses .Net's garbage collection, right? If so, that presumably rules out its use on hard real-time systems. > the Fibonacci example in the online tutorial For anyone struggling to find it, ctrl-f for completed Fibonacci I agree the Dafny syntax is very tidy. Surprisingly I wasn't able to find a directly comparable SPARK program. The closest I could manage was populating an array with the Fib sequence, by someone on StackOverflow (I haven't verified it) [0] [0] https://stackoverflow.com/a/57169728/ https://stackoverflow.com/a/57169728/
- twoWhlsGud 6y ago
  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
- mcguire 6y ago
  "I forgot to ask an obvious question: Dafny uses .Net's garbage collection, right? If so, that presumably rules out its use on hard real-time systems." I was just about to point that out. Yes, Dafny uses garbage collection (which makes formal verification much easier). As far as I know in SPARK (and FRAMA-C), verification of memory allocation is still an open research question.
rurban 6y ago
Sure it does have native targets. It can compile to C++, Go, JS, and many more. And you forgot that Dafny has Microsoft behind, so I would rate it ahead of Spark ADA. Visual Studio support. It also has a much nicer syntax, also compared to ATS, which is in the same league.
- dwohnitmok 6y ago
  But are those backends complete? I.e. do they support all of Dafny? Last I programmed in Dafny I don't think any alternative back end did. Also Dafny has pretty poor IDE support. I don't think it has Visual Studio support and the plugin for Visual Studio Code is not written by MS (and is pretty bare bones). MS really only supports Dafny by employing its creator. It doesn't seem to devote any other resources. Again I haven't programmed with SPARK before but my impression is that it's getting way more industry use and support.
  - MaxBarraclough 6y ago
    > Again I haven't programmed with SPARK before but my impression is that it's getting way more industry use and support. Correct, it's been used in numerous life-or-death systems. Perhaps most famously, the software of the Boeing 777 is almost entirely SPARK based. [0][1] Dafny has not, it seems to be more of a research project. > MS really only supports Dafny by employing its creator. It doesn't seem to devote any other resources. Right. It would be interesting if Microsoft decided to compete in the critical-systems space, but I doubt they will. With SPARK Ada, all the real work seems to happen at AdaCore. [2] There are various different high-assurance Ada compilers available though. [0] https://www.cse.msu.edu/~cse814/Lectures/09_spark_intro.pdf https://www.cse.msu.edu/~cse814/Lectures/09_spark_intro.pdf [1] https://www.ei.tum.de/fileadmin/tueifei/rcs/becker/spark2014-intro.pdf https://www.ei.tum.de/fileadmin/tueifei/rcs/becker/spark2014... [2] https://www.adacore.com/ https://www.adacore.com/

MaxBarraclough 6y ago

> I doubt Dafny will have native targets (which I assume is a prerequisite for the "critical-systems" work you're talking about) any time soon if ever Fair enough. Still a really neat project. I forgot to ask an obvious question: Dafny uses .Net's garbage collection, right? If so, that presumably rules out its use on hard real-time systems. > the Fibonacci example in the online tutorial For anyone struggling to find it, ctrl-f for completed Fibonacci I agree the Dafny syntax is very tidy. Surprisingly I wasn't able to find a directly comparable SPARK program. The closest I could manage was populating an array with the Fib sequence, by someone on StackOverflow (I haven't verified it) [0] [0] https://stackoverflow.com/a/57169728/ https://stackoverflow.com/a/57169728/

twoWhlsGud 6y ago
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
mcguire 6y ago
"I forgot to ask an obvious question: Dafny uses .Net's garbage collection, right? If so, that presumably rules out its use on hard real-time systems." I was just about to point that out. Yes, Dafny uses garbage collection (which makes formal verification much easier). As far as I know in SPARK (and FRAMA-C), verification of memory allocation is still an open research question.

rurban 6y ago

Sure it does have native targets. It can compile to C++, Go, JS, and many more. And you forgot that Dafny has Microsoft behind, so I would rate it ahead of Spark ADA. Visual Studio support. It also has a much nicer syntax, also compared to ATS, which is in the same league.

dwohnitmok 6y ago
But are those backends complete? I.e. do they support all of Dafny? Last I programmed in Dafny I don't think any alternative back end did. Also Dafny has pretty poor IDE support. I don't think it has Visual Studio support and the plugin for Visual Studio Code is not written by MS (and is pretty bare bones). MS really only supports Dafny by employing its creator. It doesn't seem to devote any other resources. Again I haven't programmed with SPARK before but my impression is that it's getting way more industry use and support.
- MaxBarraclough 6y ago
  > Again I haven't programmed with SPARK before but my impression is that it's getting way more industry use and support. Correct, it's been used in numerous life-or-death systems. Perhaps most famously, the software of the Boeing 777 is almost entirely SPARK based. [0][1] Dafny has not, it seems to be more of a research project. > MS really only supports Dafny by employing its creator. It doesn't seem to devote any other resources. Right. It would be interesting if Microsoft decided to compete in the critical-systems space, but I doubt they will. With SPARK Ada, all the real work seems to happen at AdaCore. [2] There are various different high-assurance Ada compilers available though. [0] https://www.cse.msu.edu/~cse814/Lectures/09_spark_intro.pdf https://www.cse.msu.edu/~cse814/Lectures/09_spark_intro.pdf [1] https://www.ei.tum.de/fileadmin/tueifei/rcs/becker/spark2014-intro.pdf https://www.ei.tum.de/fileadmin/tueifei/rcs/becker/spark2014... [2] https://www.adacore.com/ https://www.adacore.com/