3 ms·

No, they can be checked in many different ways, hence their power. Sure, but the more dynamic ones that drift away from what a (good) static type system offers

No, they can be checked in many different ways, hence their power. Sure, but the more dynamic ones that drift away from what a (good) static type system offers are exactly the ones that aren't amenable to automated proofs and so tend to be checked at run time. Such programs often use formal methods that precisely use such contracts. Rich type systems (like Idris's) are virtually never used in practice in those cases. As someone who has worked on relatively high-reliability systems, I can say with 100% confidence: it depends. This too is an area with a whole spectrum of possibilities, and some of those involve a degree of formal proof of algorithm properties but not a mechanically verified translation of those algorithms into implementation code. In such cases, a powerful static type system certainly can be a useful safeguard against introducing defects during the translation.

pron 7y ago
> Sure, but the more dynamic ones that drift away from what a (good) static type system offers are exactly the ones that aren't amenable to automated proofs and so tend to be checked at run time. Not really. What contract systems allow you to do is to separate specification from verification. Type systems require that all of your specifications be verified with deductive proofs. This means that some deep properties either require a lot of work (using a type system such as Idris's) or are excluded from the type system at all. Contracts allow you to check a property in unsound ways, too. As far as correctness is concerned, contracts do everything a type system can, but more flexibly. Type systems, however, have advantages related to tooling and efficient code generation by an AOT compiler. > This too is an area with a whole spectrum of possibilities, and some of those involve a degree of formal proof of algorithm properties but not a mechanically verified translation of those algorithms into implementation code. Even when formal proofs are used, the specification is done in a contract system, not a dependent type system.
- Silhouette 7y ago
  What contract systems allow you to do is to separate specification from verification. Type systems require that all of your specifications be verified with deductive proofs. I think you're making the same point that I am, but perhaps from the opposite direction. Of course contracts are more general, but the aspects of a contract that you can prove automatically in advance are similar to what you can typically do with a good static type system, and the limits of a decent static type system fall around the point that contracts become more powerful but only at runtime. This isn't an accident, it's a fundamental equivalence. For example, you mentioned SPARK before. One of the interesting things about SPARK is the extra flexibility you have when adding constraints on integer data types. The proof system can verify certain properties (or warn you that it can't). That can provide safeguards against, among other things, some very common logic errors like out-of-bounds access to data structures. However, the fact that we're dealing with integer values is very helpful in this respect. Lots of behaviour is fully specified no matter how much we manipulate those values. For the same reason, dependent type systems can often provide similar guarantees. The curious property of C++ templates that they allow integer as well as type parameters has allowed for all kinds of handy metaprogramming tricks along similar lines. Now, suppose we're working in the much less convenient world of floating point values. It's still helpful to have warnings about, for example, potential underflow or overflow conditions, for all the same reasons. However, given the inherent imprecision of floating point data, it is impossible to prove such conditions in advance in almost any non-trivial case. You can certainly have a precondition on a relevant function that, for example, adding two input values must not entirely lose the smaller value due to loss of significance, but you won't find out about inputs that violate the contract until you run your program. Even when formal proofs are used, the specification is done in a contract system, not a dependent type system. You can do the specification in any number of ways. Unless you want to classify all of mathematics as "a contract system", which is true in a sense but so general as to lose any useful meaning of the term, your statement above is too strong.

pron 7y ago

> Sure, but the more dynamic ones that drift away from what a (good) static type system offers are exactly the ones that aren't amenable to automated proofs and so tend to be checked at run time. Not really. What contract systems allow you to do is to separate specification from verification. Type systems require that all of your specifications be verified with deductive proofs. This means that some deep properties either require a lot of work (using a type system such as Idris's) or are excluded from the type system at all. Contracts allow you to check a property in unsound ways, too. As far as correctness is concerned, contracts do everything a type system can, but more flexibly. Type systems, however, have advantages related to tooling and efficient code generation by an AOT compiler. > This too is an area with a whole spectrum of possibilities, and some of those involve a degree of formal proof of algorithm properties but not a mechanically verified translation of those algorithms into implementation code. Even when formal proofs are used, the specification is done in a contract system, not a dependent type system.

Silhouette 7y ago
What contract systems allow you to do is to separate specification from verification. Type systems require that all of your specifications be verified with deductive proofs. I think you're making the same point that I am, but perhaps from the opposite direction. Of course contracts are more general, but the aspects of a contract that you can prove automatically in advance are similar to what you can typically do with a good static type system, and the limits of a decent static type system fall around the point that contracts become more powerful but only at runtime. This isn't an accident, it's a fundamental equivalence. For example, you mentioned SPARK before. One of the interesting things about SPARK is the extra flexibility you have when adding constraints on integer data types. The proof system can verify certain properties (or warn you that it can't). That can provide safeguards against, among other things, some very common logic errors like out-of-bounds access to data structures. However, the fact that we're dealing with integer values is very helpful in this respect. Lots of behaviour is fully specified no matter how much we manipulate those values. For the same reason, dependent type systems can often provide similar guarantees. The curious property of C++ templates that they allow integer as well as type parameters has allowed for all kinds of handy metaprogramming tricks along similar lines. Now, suppose we're working in the much less convenient world of floating point values. It's still helpful to have warnings about, for example, potential underflow or overflow conditions, for all the same reasons. However, given the inherent imprecision of floating point data, it is impossible to prove such conditions in advance in almost any non-trivial case. You can certainly have a precondition on a relevant function that, for example, adding two input values must not entirely lose the smaller value due to loss of significance, but you won't find out about inputs that violate the contract until you run your program. Even when formal proofs are used, the specification is done in a contract system, not a dependent type system. You can do the specification in any number of ways. Unless you want to classify all of mathematics as "a contract system", which is true in a sense but so general as to lose any useful meaning of the term, your statement above is too strong.