[plt-scheme] HTDP: Ought folks use contracts while working through HTDP?

History:

I introduced the word contract in 1995 or 6 to distinguish the  
comments in HtDP from types and yet to allude to something like types.

To use the word "type" is only meaningful in a context where a  
language of types is clearly defined and a mechanism for checking  
whether an expresssion E is classifiable as something that satisfies  
type T exists. (That's theorem checking.)

Scheme had no type system at the time, and I didn't want a type  
system. Typical novices say for the first few weeks "the computer did  
this to me". No need to introduce yet another level of syntactic  
detail, no need to introduce yet another level of failure at this point.

At the same time, I strongly believe that the organization of  
functions is best based on something like types. A naive and  
intuitive notion of set-based reasoning comes in handy here. They are  
easy to express with a mix of English and constructors from whatever  
language you choose (Scheme, Perl, Python). They are intuitive to  
reason with and about. And I hoped they'd be easy to check,  
dynamically first and statically second.

Robby explored the dynamic, formal counter-parts to this notion of  
"contracts" in his dissertation.

Sam is exploring the static, formal counter-part and complement to  
Robby's type with Typed Scheme.

One day we're hoping to have a smooth path from untyped Scheme to  
Scheme with contracts and types.

-- Matthias








On Sep 3, 2008, at 9:30 AM, Grant Rettke wrote:

> Hi folks,
>
> Should people working on HTDP be welcome to include contracts
>
> http://pre.plt-scheme.org/plt/doc/guide/contracts.html
>
> to specify the behavior of functions that they implement?
>
> Best wishes,
>
> Grant
> _________________________________________________
>   For list-related administrative tasks:
>   http://list.cs.brown.edu/mailman/listinfo/plt-scheme