[Solved]: Is Wadler’s ‘Theorems for Free’ as general as Design By Contract for establishing correctness?

ignougroup
Problem Detail: 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)

Asked By : hawkeye

Answered By : Uday Reddy

“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.
Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/19135