Lambda the Ultimate

A Functional I/O System (or Fun for Freshman Kids), by Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, and Shriram Krishnamurthi. ICFP 2009.

Functional programming languages ought to play a central role in mathematics education for middle schools (age range: 10­-14). After all, functional programming is a form of algebra and programming is a creative activity about problem solving. Introducing it into mathematics courses would make pre-algebra course come alive. If input and output were invisible, students could implement fun simulations, animations, and even interactive and distributed games all while using nothing more than plain mathematics.

We have implemented this vision with a simple framework for purely functional I/O. Using this framework, students design, implement, and test plain mathematical functions over numbers, booleans, string, and images. Then the framework wires them up to devices and performs all the translation from external information to internal data (and vice versa) -- just like every other operating system. Once middle school students are hooked on this form of programming, our curriculum provides a smooth path for them from pre-algebra to freshman courses in college on object-oriented design and theorem proving.

This is a paper explaining some of the technical underpinnings of the How to Design Worlds curriculum that the PLT group has worked on.

I was tempted to categorize this as "functional", but decided against it. One of the really nice features of this curriculum is actually its applicability to imperative programming. Here, students are taught to think of interactive programs as functions written in world-passing style, and to specify programs in terms of the invariants that the function maintains on the world data.

That is: students are taught about loop invariants, without ever having to write an explicit loop. In my experience, loop invariants are the most difficult part of explaining Hoare logic (and hence of explaining imperative programming), because they require imagining a dynamic picture of what the static source code will eventually do. This style of teaching helps to manage that difficulty by making the dynamic state into visible animations.