3 ms·

Imperative and functional programming languages have gone in different directions with respect to proving program correctness. I'm not sure one path is clearly

Imperative and functional programming languages have gone in different directions with respect to proving program correctness. I'm not sure one path is clearly better than another, they're just different. The imperative world has languages like Dafny or Whiley, where functions are annotated with expressions denoting things that must be true, and the compiler does theorem proving to ensure that the constraints aren't violated. So rather than put things like "length of array A equals length of array B" into types, you put that rule into the code, and the compiler proves that the constraint always holds. Unfortunately all these languages aren't really mature, whether they use dependent types or contracts. The imperative versions in particular often need you to specify constraints that are obvious.

pron 8y ago
> The imperative world has languages like Dafny or Whiley, where functions are annotated with expressions denoting things that must be true, and the compiler does theorem proving to ensure that the constraints aren't violated. We have that for Java, too: http://www.openjml.org/ http://www.openjml.org/ The great thing about contracts (as opposed to dependent types) is that they separate specification from verification. You could use proofs (fully- or semi-automatic), but you could also use weaker but cheaper forms of verification, such as concolic tests or randomized tests, generated from the contracts, or, weaker still, runtime assertions. Dependent types tie specification to a specific form of verification (proof). A standardized specification language like JML can (and does) have many tools offering different forms of verification.
mcguire 8y ago
In addition to Dafny (https://github.com/Microsoft/dafny https://github.com/Microsoft/dafny) and Whiley (http://whiley.org/ http://whiley.org/), check out Frama-C (https://frama-c.com/ https://frama-c.com/) for C and SPARK (http://www.spark-2014.org/ http://www.spark-2014.org/) for Ada. Both are mature enough to be in use, but are limited primarily by the fact that both languages have manual memory management, which is well understood via separation logic, but poorly supported by the tools. I've written some blog posts about Frama-C: * https://maniagnosis.crsr.net/2017/06/AFL-brute-force-search.html https://maniagnosis.crsr.net/2017/06/AFL-brute-force-search.... * https://maniagnosis.crsr.net/2017/06/AFL-bug-in-quicksearch.html https://maniagnosis.crsr.net/2017/06/AFL-bug-in-quicksearch.... * https://maniagnosis.crsr.net/2017/07/AFL-correctness-of-quicksearch.html https://maniagnosis.crsr.net/2017/07/AFL-correctness-of-quic... * https://maniagnosis.crsr.net/2017/08/AFL-verifying-quicksort.html https://maniagnosis.crsr.net/2017/08/AFL-verifying-quicksort...

pron 8y ago

> The imperative world has languages like Dafny or Whiley, where functions are annotated with expressions denoting things that must be true, and the compiler does theorem proving to ensure that the constraints aren't violated. We have that for Java, too: http://www.openjml.org/ http://www.openjml.org/ The great thing about contracts (as opposed to dependent types) is that they separate specification from verification. You could use proofs (fully- or semi-automatic), but you could also use weaker but cheaper forms of verification, such as concolic tests or randomized tests, generated from the contracts, or, weaker still, runtime assertions. Dependent types tie specification to a specific form of verification (proof). A standardized specification language like JML can (and does) have many tools offering different forms of verification.

mcguire 8y ago

In addition to Dafny (https://github.com/Microsoft/dafny https://github.com/Microsoft/dafny) and Whiley (http://whiley.org/ http://whiley.org/), check out Frama-C (https://frama-c.com/ https://frama-c.com/) for C and SPARK (http://www.spark-2014.org/ http://www.spark-2014.org/) for Ada. Both are mature enough to be in use, but are limited primarily by the fact that both languages have manual memory management, which is well understood via separation logic, but poorly supported by the tools. I've written some blog posts about Frama-C: * https://maniagnosis.crsr.net/2017/06/AFL-brute-force-search.html https://maniagnosis.crsr.net/2017/06/AFL-brute-force-search.... * https://maniagnosis.crsr.net/2017/06/AFL-bug-in-quicksearch.html https://maniagnosis.crsr.net/2017/06/AFL-bug-in-quicksearch.... * https://maniagnosis.crsr.net/2017/07/AFL-correctness-of-quicksearch.html https://maniagnosis.crsr.net/2017/07/AFL-correctness-of-quic... * https://maniagnosis.crsr.net/2017/08/AFL-verifying-quicksort.html https://maniagnosis.crsr.net/2017/08/AFL-verifying-quicksort...