4 ms·

Code-level specifications (sometimes called contracts) that can be verified by various means (including manual deductive proofs, and automated solvers) exist fo

by pron 8y ago

Code-level specifications (sometimes called contracts) that can be verified by various means (including manual deductive proofs, and automated solvers) exist for mainstream programming languages. The most mature ones are probably JML for Java (verified with https://www.openjml.org/ https://www.openjml.org/ and various other tools) and ACSL for C (verified with https://frama-c.com/ https://frama-c.com/). C# has Spec#, but I'm not sure it's still used. It is still unclear how best to use such code level verification, as the effort required grows very quickly with code size, and it's unclear how much sporadic verification of properties that are easy to prove actually improves correctness, but this is all still ongoing research.

garethrowlands 8y ago
Often it's best to just express preconditions in the normal types. For example, instead of having a `head-of-list` function that crashes with empty input, define its input to be of type `NonEmptyList`. Refinement types are also worth exploring in this space, as they appear to give a good power-to-weight. See Liquid Haskell, for example, https://ucsd-progsys.github.io/liquidhaskell-tutorial/03-basic.html https://ucsd-progsys.github.io/liquidhaskell-tutorial/03-bas...
- pron 8y ago
  The power-to-weight ratio of refinement types is as unclear as that of contracts. You get more expressivity than simple types, but it's unclear whether it's enough to make a real impact. On the other hand, we're nowhere near being able to verify the properties that would make a real impact on code sizes that truly matter with automated proof techniques. Types are a bad fit for "deep" properties to begin with because they're tied to the proof theory of the type system. At least contracts have some leeway, as they can be verified more weakly but with much more scalable techniques (like randomized tests).

by pron 8y ago

garethrowlands 8y ago

Often it's best to just express preconditions in the normal types. For example, instead of having a `head-of-list` function that crashes with empty input, define its input to be of type `NonEmptyList`. Refinement types are also worth exploring in this space, as they appear to give a good power-to-weight. See Liquid Haskell, for example, https://ucsd-progsys.github.io/liquidhaskell-tutorial/03-basic.html https://ucsd-progsys.github.io/liquidhaskell-tutorial/03-bas...

pron 8y ago
The power-to-weight ratio of refinement types is as unclear as that of contracts. You get more expressivity than simple types, but it's unclear whether it's enough to make a real impact. On the other hand, we're nowhere near being able to verify the properties that would make a real impact on code sizes that truly matter with automated proof techniques. Types are a bad fit for "deep" properties to begin with because they're tied to the proof theory of the type system. At least contracts have some leeway, as they can be verified more weakly but with much more scalable techniques (like randomized tests).