Re: Curl, multiple inheritance, and interfaces (was Re: cheerful static typing)

[Shriram Krishnamurthi <address@hidden>]

Lennon Day-Reynolds wrote:

> Now, back to the tools that are fun to hack with...

Hey -- Specware is great fun to hack with!  You just need to know
category theory as a second language (-:.

One of the doyens of theorem proving (John Rushby?) has a notion that
one way to get kids hooked on formalism is to present it as a game in
high school.  Trying to get a lemma past the vagaries of a theorem
prover can be just as addictive, not to mention as much fun, as trying
to figure out where the golden goblet that charms the magic amulet
resides -- it's just never presented that way.  (Induction?  Sequents?
Resolution?  Blecch!)

I'm sure there are some school-level games that apply this principle.
A more pedantic example is Barwise and Etchemendy's Hyperproof, which
drills natural deduction through a visual world of solid objects.
There's a game in there somewhere.  ("Now Lara Croft, about to be
crushed by the large red sphere rolling her way, reaches into her
backpack and yanks out ... modus ponens!")

Shriram