2
$\begingroup$

Philip Wadler has written a brilliant paper called 'Theorems for Free'. The big idea is that you can use types to reason about your program, and even prove simple theorems about your program.

We see these ideas about types applied in the Haskell language.

At very roughly the same time period - we have an idea from Betrand Meyer called 'Design By Contract'- which is most notably implemented in the Eiffel Language. This has the following features:

  • routine preconditions
  • routine postconditions
  • class invariants
  • check instructions (like assert)
  • loop invariants

The idea behind Design by Contract is software designers should define formal, precise and verifiable interface specifications for software components, which extend the ordinary definition of abstract data types with preconditions, postconditions and invariants.

Now many claim that using 'Types' in your programs leads to 'more correct programs' (via the Howard Curry Correspondence). From what I can see - even the most advanced use of Dependent Typing in Idris and Scala is limited to Sum Types and list lengths (correct me if I'm wrong).

By contrast - the power of 'Design By Contract' in establishing the correctness of my program is more general and more powerful. (Albeit not necessarily at compile-time - but at test time). I can for example establish in my banking program that all deposits are positive, and all reported account balances are positive.

The point being - types have a fascinating future of possibilities, and are enormously powerful and compile time - but right now their practical application seems limited.

My question is: is design by contract of more general application than using theorems from types to reason about the correctness of my program at present? (Or are we just talking about two different things)

$\endgroup$
3
$\begingroup$

"Theorems for free" are so-called because they follow from the type of the program, without looking at the the program code!

"Contracts" are clearly not free theorems, because they depend on the code of the program, not merely the type.

However, the connection you do want to make is between types and specifications. Specifications are in a way "more detailed" types. Or, state the other way, types are more basic specifications. Martin-Lof type theory is precisely about fusing the two ideas into one.

$\endgroup$
  • $\begingroup$ Can you provide a link or reference to the last point about Martin-Lof type theory fusing the two ideas? (Apart from the wikipedia page) $\endgroup$ – hawkeye Feb 5 '14 at 22:36
  • 1
    $\begingroup$ @hawkeye. See the "further reading" list on the Wiki page, especially the book by Simon Thompson. There is a machine implementation of Martin-Lof type theory called Agda, which is widely used. You can download it and play with it. $\endgroup$ – Uday Reddy Feb 5 '14 at 22:40
1
$\begingroup$

The power of "theorems for free" depends upon the type system you choose to use. But as it is typically used, yes, "design by contract" is more expressive than "theorems for free": "design by contract" lets you specify some properties that cannot easily be proven using the "theorems for free" approach. Of course that does not mean that the "theorems for free" idea is useless or uninteresting.

I think maybe you are thinking about this in not quite the right way. It sounds almost like you are looking for a silver bullet or The One True Path to program correctness. Personally, I doubt that there will be any one-size-fits-all answer that is a perfect solution. Instead, I suggest that you focus more on understanding the space of available techniques and getting a better grip on their strengths and weaknesses -- I think you'll find that more informative than trying to set up a "gorilla vs shark" dichotomy ("theorems for free vs design by contract -- in a fight between the two, who would win?").

$\endgroup$
  • $\begingroup$ I appreciate the thoughtfulness and balance in your answer $\endgroup$ – hawkeye Dec 20 '13 at 6:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.