3 ms·

My guess is that types would be better for enforcing code organization and for tooling ... while contracts are better for correctness I see what you're getting

My guess is that types would be better for enforcing code organization and for tooling ... while contracts are better for correctness I see what you're getting at, but there is one other crucial difference: the types we're talking about here are usually checked at compile time, whereas the contracts we're talking about here are usually checked at run time. Although the latter may be more expressive if other things are equal, other things are very much not equal in this respect. How much that matters depends on the nature of the software and how it is to be deployed and used. If you're writing a program for your own use, it might not matter much at all. If you're writing a program that is going to control a satellite and software maintenance after launch is extremely expensive if not impossible, it might matter a great deal.

pron 7y ago
> whereas the contracts we're talking about here are usually checked at run time No, they can be checked in many different ways, hence their power. They can be checked "statically", i.e. at compile-time, or dynamically. One approach is sound but requires more effort, while the other is cheap yet unsound -- and there is a spectrum in between the two extremes. > If you're writing a program that is going to control a satellite and software maintenance after launch is extremely expensive if not impossible, it might matter a great deal. 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. If you've heard of SPARK, it's a language that provides static verification of properties specified as contracts, not as part of the type system, and it is used in some safety-critical realtime applications.
- Silhouette 7y ago
  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

> whereas the contracts we're talking about here are usually checked at run time No, they can be checked in many different ways, hence their power. They can be checked "statically", i.e. at compile-time, or dynamically. One approach is sound but requires more effort, while the other is cheap yet unsound -- and there is a spectrum in between the two extremes. > If you're writing a program that is going to control a satellite and software maintenance after launch is extremely expensive if not impossible, it might matter a great deal. 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. If you've heard of SPARK, it's a language that provides static verification of properties specified as contracts, not as part of the type system, and it is used in some safety-critical realtime applications.

Silhouette 7y ago
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.