6 ms·

What are the competitors to this language? Can someone provide a list. I'd like to start learning a provable language, not sure if Dafny is the one I should sta

by didibus 10y ago

What are the competitors to this language? Can someone provide a list. I'd like to start learning a provable language, not sure if Dafny is the one I should start with though.

Kametrixom 10y ago
Check out Idris maybe
Devagamster 10y ago
Coq is the one I use most. I've heard of lean as well though. Those are both proof assistants not theorem provers. Dafny uses z3 to attempt to automatically prove theorems about your code. Lean or Coq (for the most part) require that you write the proofs manually in a special language they provide and they will tell you whether or not your proof has errors. In general these languages lie on a spectrum between more automatic to more manual with the automatic ones taking potentially more time and being more limited but requiring less of you and the manual ones such as lean or coq are more expressive but harder to use because you have to provide all of the proofs. I should say all this with the caveat that I'm only learning these things now so I've probably said something wrong. Please correct me if that is the case.
profquail 10y ago
Isabelle is another language for program verification / theorem proving, similar to Dafny and Coq: https://isabelle.in.tum.de/ https://isabelle.in.tum.de/
nickpsecurity 10y ago
SPARK Ada is the main competitor & has been in industrial use a long time: http://www.spark-2014.org/uploads/itp_2014_r610.pdf http://www.spark-2014.org/uploads/itp_2014_r610.pdf http://www.anthonyhall.org/c_by_c_secure_system.pdf http://www.anthonyhall.org/c_by_c_secure_system.pdf http://libre.adacore.com/tools/spark-gpl-edition/ http://libre.adacore.com/tools/spark-gpl-edition/
SilasX 10y ago
Per this reddit comment [1], the languages supporting some kind of compile-time constraint-checking/proving include Why3, Dafny, Fstar, Coq, Agda, and Idris. Also, some languages have been extended to support it: LiquidHaskell, Frama-C, and Spark/Ada. I also recall some Java extension but can't find it atm. [1] https://www.reddit.com/r/ProgrammingLanguages/comments/4ref8v/can_pls_have_richer_more_general_compiletime/d50gwpb/?utm_content=permalink&utm_medium=front&utm_source=reddit&utm_name=ProgrammingLanguages https://www.reddit.com/r/ProgrammingLanguages/comments/4ref8...
- tom_mellior 10y ago
  > I also recall some Java extension but can't find it atm. You might be thinking of JML (Java Modeling Language): http://www.eecs.ucf.edu/~leavens/JML//index.shtml http://www.eecs.ucf.edu/~leavens/JML//index.shtml Apparently JML-annotated programs can passed to Why3 using a confusingly documented set of tools: http://krakatoa.lri.fr/ http://krakatoa.lri.fr/ There is also the Cheker Framework for Java: http://types.cs.washington.edu/checker-framework/ http://types.cs.washington.edu/checker-framework/ But as far as I understand it's less general than all the other tools you mention.
  - tom_mellior 10y ago
    Also, and probably even more likely than the ones I mentioned above, there is KeY for Java verification: http://www.key-project.org/index.php http://www.key-project.org/index.php
- igravious 10y ago
  Per the Wikipedia page for Whiley[1] the languages akin to Dafny are mentioned when explaining what Whiley is: “The primary purpose of such a tool is to improve software quality by ensuring a program meets a formal specification. In other words, to help identify and eliminate software bug in the programs being developed. Whiley follows many attempts to develop such tools, including notable efforts such as SPARK/Ada, ESC/Java, Spec#, Dafny, Why3 and Frama-C.” I'm thinking there must be a reason they do not mention F*, Coq, Agda, and Idris, perhaps because they are proof assistants[2] rather than automatic provers of programs with formal specifications. See also Isabelle and others. Regarding Idris (which you mention but is not on that page) and Epigram (which is noteworthy and again not on that page), neither are production ready and the latter is unmaintained. [1] https://en.wikipedia.org/wiki/Whiley_(programming_language)#Overview https://en.wikipedia.org/wiki/Whiley_(programming_language)#... [2] https://en.wikipedia.org/wiki/Proof_assistant https://en.wikipedia.org/wiki/Proof_assistant
gergoerdi 10y ago
There's the so-called 'B Method', which seems very similar to this on the programming language side. I haven't checked the proof language so that may be very different. I've got a two-parter on my blog giving a glimpse of B's programming language[1] and proof language[2]. [1] https://gergo.erdi.hu/blog/2010-02-16-the_b_method_for_programmers_(part_1)/ https://gergo.erdi.hu/blog/2010-02-16-the_b_method_for_progr... [2] https://gergo.erdi.hu/blog/2010-02-22-the_b_method_for_programmers_(part_2)/ https://gergo.erdi.hu/blog/2010-02-22-the_b_method_for_progr...
bjz_ 10y ago
http://whiley.org/ http://whiley.org/ is another similar language that uses an SMT solver for testing program invariants.
xearl 10y ago
Perfect Developer [1] is another one not yet mentioned. You write and verify your "specifications" (program-parts to be verified) using a language called "Perfect" and generate C++, C#, or Java from that (SPARK Ada generator in progress). [1] http://www.eschertech.com/products/perfect_developer.php http://www.eschertech.com/products/perfect_developer.php
tomp 10y ago
One of the most serious competitors is F* - it's even based on the same underlying technology (Z3) but uses a more ML-like syntax. https://fstar-lang.org/ https://fstar-lang.org/
- didibus 10y ago
  F* looks pretty neat. I might try to learn that one.
qznc 10y ago
It is a gradual range from untyped (assembly) to proof-anything (Isabelle, Coq). The more interesting question is: Where are the sweet spots? The current mainstream (Java,C++,etc) form a big cluster "sweetrange" of roughly equivalent type safety. Rust with its ownership type system goes one step towards more proofs. ATS is even further. Agda and Idris want to be useable programming languages while providing as much proof as possible. Isabelle can generate code, but is also used as just a theorem prover.
- tom_mellior 10y ago
  > Rust with its ownership type system goes one step towards more proofs. Does it really, though? The ownership system only talks about ownership, which you only need to reason about due to the artificial choice of avoiding garbage collection. So yes, you get closer to proofs, but only to proofs of properties that are not necessary to prove for Java, say. You might use the ownership and lifetime system to derive must-not-alias guarantees that might help with some verification tasks, but I'm not sure how much it would help. I'd love to see a deductive verification system for Rust, but I wouldn't expect it to be the silver bullet for verification.
  - Sean1708 10y ago
    Ownership is used for more than just memory management though, concurrent memory access for example.
    - tom_mellior 10y ago
      True! I wasn't thinking beyond verification of single-threaded programs, which is hard enough as it is ;-)
  - qznc 10y ago
    There is a convert-Rust-to-Lean-for-verification project. The not-aliasing guarantees did help tremendously there. https://kha.github.io/2016/07/22/formally-verifying-rusts-binary-search.html https://kha.github.io/2016/07/22/formally-verifying-rusts-bi...
mrefj 10y ago
ACL2 http://www.cs.utexas.edu/~moore/acl2/ http://www.cs.utexas.edu/~moore/acl2/
ivcha 10y ago
Leon (http://lara.epfl.ch/w/leon http://lara.epfl.ch/w/leon) -- effectively, a verification/synthesis framework around Scala

by didibus 10y ago

What are the competitors to this language? Can someone provide a list. I'd like to start learning a provable language, not sure if Dafny is the one I should start with though.

Kametrixom 10y ago

Check out Idris maybe

Devagamster 10y ago

Coq is the one I use most. I've heard of lean as well though. Those are both proof assistants not theorem provers. Dafny uses z3 to attempt to automatically prove theorems about your code. Lean or Coq (for the most part) require that you write the proofs manually in a special language they provide and they will tell you whether or not your proof has errors. In general these languages lie on a spectrum between more automatic to more manual with the automatic ones taking potentially more time and being more limited but requiring less of you and the manual ones such as lean or coq are more expressive but harder to use because you have to provide all of the proofs. I should say all this with the caveat that I'm only learning these things now so I've probably said something wrong. Please correct me if that is the case.

profquail 10y ago

Isabelle is another language for program verification / theorem proving, similar to Dafny and Coq: https://isabelle.in.tum.de/ https://isabelle.in.tum.de/

nickpsecurity 10y ago

SPARK Ada is the main competitor & has been in industrial use a long time: http://www.spark-2014.org/uploads/itp_2014_r610.pdf http://www.spark-2014.org/uploads/itp_2014_r610.pdf http://www.anthonyhall.org/c_by_c_secure_system.pdf http://www.anthonyhall.org/c_by_c_secure_system.pdf http://libre.adacore.com/tools/spark-gpl-edition/ http://libre.adacore.com/tools/spark-gpl-edition/

SilasX 10y ago

Per this reddit comment [1], the languages supporting some kind of compile-time constraint-checking/proving include Why3, Dafny, Fstar, Coq, Agda, and Idris. Also, some languages have been extended to support it: LiquidHaskell, Frama-C, and Spark/Ada. I also recall some Java extension but can't find it atm. [1] https://www.reddit.com/r/ProgrammingLanguages/comments/4ref8v/can_pls_have_richer_more_general_compiletime/d50gwpb/?utm_content=permalink&utm_medium=front&utm_source=reddit&utm_name=ProgrammingLanguages https://www.reddit.com/r/ProgrammingLanguages/comments/4ref8...

tom_mellior 10y ago
> I also recall some Java extension but can't find it atm. You might be thinking of JML (Java Modeling Language): http://www.eecs.ucf.edu/~leavens/JML//index.shtml http://www.eecs.ucf.edu/~leavens/JML//index.shtml Apparently JML-annotated programs can passed to Why3 using a confusingly documented set of tools: http://krakatoa.lri.fr/ http://krakatoa.lri.fr/ There is also the Cheker Framework for Java: http://types.cs.washington.edu/checker-framework/ http://types.cs.washington.edu/checker-framework/ But as far as I understand it's less general than all the other tools you mention.
- tom_mellior 10y ago
  Also, and probably even more likely than the ones I mentioned above, there is KeY for Java verification: http://www.key-project.org/index.php http://www.key-project.org/index.php
igravious 10y ago
Per the Wikipedia page for Whiley[1] the languages akin to Dafny are mentioned when explaining what Whiley is: “The primary purpose of such a tool is to improve software quality by ensuring a program meets a formal specification. In other words, to help identify and eliminate software bug in the programs being developed. Whiley follows many attempts to develop such tools, including notable efforts such as SPARK/Ada, ESC/Java, Spec#, Dafny, Why3 and Frama-C.” I'm thinking there must be a reason they do not mention F*, Coq, Agda, and Idris, perhaps because they are proof assistants[2] rather than automatic provers of programs with formal specifications. See also Isabelle and others. Regarding Idris (which you mention but is not on that page) and Epigram (which is noteworthy and again not on that page), neither are production ready and the latter is unmaintained. [1] https://en.wikipedia.org/wiki/Whiley_(programming_language)#Overview https://en.wikipedia.org/wiki/Whiley_(programming_language)#... [2] https://en.wikipedia.org/wiki/Proof_assistant https://en.wikipedia.org/wiki/Proof_assistant

gergoerdi 10y ago

There's the so-called 'B Method', which seems very similar to this on the programming language side. I haven't checked the proof language so that may be very different. I've got a two-parter on my blog giving a glimpse of B's programming language[1] and proof language[2]. [1] https://gergo.erdi.hu/blog/2010-02-16-the_b_method_for_programmers_(part_1)/ https://gergo.erdi.hu/blog/2010-02-16-the_b_method_for_progr... [2] https://gergo.erdi.hu/blog/2010-02-22-the_b_method_for_programmers_(part_2)/ https://gergo.erdi.hu/blog/2010-02-22-the_b_method_for_progr...

bjz_ 10y ago

http://whiley.org/ http://whiley.org/ is another similar language that uses an SMT solver for testing program invariants.

xearl 10y ago

Perfect Developer [1] is another one not yet mentioned. You write and verify your "specifications" (program-parts to be verified) using a language called "Perfect" and generate C++, C#, or Java from that (SPARK Ada generator in progress). [1] http://www.eschertech.com/products/perfect_developer.php http://www.eschertech.com/products/perfect_developer.php

tomp 10y ago

One of the most serious competitors is F* - it's even based on the same underlying technology (Z3) but uses a more ML-like syntax. https://fstar-lang.org/ https://fstar-lang.org/

didibus 10y ago
F* looks pretty neat. I might try to learn that one.

qznc 10y ago

It is a gradual range from untyped (assembly) to proof-anything (Isabelle, Coq). The more interesting question is: Where are the sweet spots? The current mainstream (Java,C++,etc) form a big cluster "sweetrange" of roughly equivalent type safety. Rust with its ownership type system goes one step towards more proofs. ATS is even further. Agda and Idris want to be useable programming languages while providing as much proof as possible. Isabelle can generate code, but is also used as just a theorem prover.

tom_mellior 10y ago
> Rust with its ownership type system goes one step towards more proofs. Does it really, though? The ownership system only talks about ownership, which you only need to reason about due to the artificial choice of avoiding garbage collection. So yes, you get closer to proofs, but only to proofs of properties that are not necessary to prove for Java, say. You might use the ownership and lifetime system to derive must-not-alias guarantees that might help with some verification tasks, but I'm not sure how much it would help. I'd love to see a deductive verification system for Rust, but I wouldn't expect it to be the silver bullet for verification.
- Sean1708 10y ago
  Ownership is used for more than just memory management though, concurrent memory access for example.
  - tom_mellior 10y ago
    True! I wasn't thinking beyond verification of single-threaded programs, which is hard enough as it is ;-)
- qznc 10y ago
  There is a convert-Rust-to-Lean-for-verification project. The not-aliasing guarantees did help tremendously there. https://kha.github.io/2016/07/22/formally-verifying-rusts-binary-search.html https://kha.github.io/2016/07/22/formally-verifying-rusts-bi...

mrefj 10y ago

ACL2 http://www.cs.utexas.edu/~moore/acl2/ http://www.cs.utexas.edu/~moore/acl2/

ivcha 10y ago

Leon (http://lara.epfl.ch/w/leon http://lara.epfl.ch/w/leon) -- effectively, a verification/synthesis framework around Scala