[TYPES] teaching discrete math and logic to undergraduates

[Matthias Felleisen]

On Aug 21, 2009, at 5:36 PM, Jean Gallier wrote:

> For now three years, I have been teaching a Discrete Math course
> for undergraduates. I believe that it is important to expose these  
> kids
> to logic, ...

Agreed!

On this note, some three years ago NEU started teaching a
follow-up spring-semester course to Discrete Mathematics that
introduces _freshmen_ to theorem proving about code. We use ACL2,
which  nicely fits to the design discipline we teach with Scheme/"How
to  Design Programs" in the first (fall) course. In our dialect of
ACL2 students can write interactive video games in a functional
language and can them prove theorems about the actual running code.
The proof discipline matches the design discipline and prepares
students for reasoning about abstract/virtual machines.

While my graduate students and I started the course, Pete
Manolios (cc'ed) has taken over and has delivered the course
for the past two years. I am sure he can point interested parties
to relevant web pages (privately or if there's enough interest
on the list).

-- Matthias