Re: peasant revolt against DrScheme!

[sperber@informatik.uni-tuebingen.de (Michael Sperber [Mr. Preprocessor])]

>>>>> "Matthias" == Matthias Felleisen <matthias@cs.rice.edu> writes:

Matthias> P.S. If you really do inductive proofs in the first course (which I
Matthias> understand from my German background, but which I think is a
Matthias> mistake)

Maybe so.  Unfortunately, our fucked-up curriculcum doesn't really
give us any choice.  If we don't do it in intro CS, it doesn't happen.

Matthias> you may wish to set out for two things: 

Matthias>  1. The definitions of lists trees etc are structurally inductive. 
Matthias>     Use them. 

Absolutely.

Matthias>  2. In my long history of doing theoretical CS, I have
Matthias>     hardly ever used induction on natural numbers. Anyone
Matthias>     else? Get them used to structural induction right
Matthias>     away. It's yet another reason to match the structure of
Matthias>     the DD with the structure of the Program. (Rich Clements
Matthias>     didn't in his recent post, but we all understand :-)

Absolutely.

-- 
Cheers =8-} Mike
Friede, Völkerverständigung und überhaupt blabla