[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Curl, multiple inheritance, and interfaces (was Re: cheerful static typing)
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?
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!")