Lambda the Ultimate

Ross Anderson and Roger Needham, 1995. Programming Satan’s Computer. In J. van Leeuwen, editor, Computer Science Today, LNCS 1000, pages 426-440.

Cryptographic protocols are used in distributed systems to identify users and authenticate transactions. They may involve the exchange of about 2–5 messages, and one might think that a program of this size would be fairly easy to get right. However, this is absolutely not the case: bugs are routinely found in well known protocols, and years after they were first published. The problem is the presence of a hostile opponent, who can alter messages at will. In effect, our task is to program a computer which gives answers which are subtly and maliciously wrong at the most inconvenient possible moment. This is a fascinating problem; and we hope that the lessons learned from programming Satan’s computer may be helpful in tackling the more common problem of programming Murphy’s.

Incidentally, the first edition of Anderson's book, Security Engineering, Wiley, 2001, is available for download.

...a domain specific language for simulating football. ... We have used Soccer-Fun in teaching during the past four years. We have also experience in using Soccer-Fun for pupils in secondary education. ... It engages students to problem solving with functional programming because it allows them to compete at several disciplines: the best performing football team can become champion of a tournament; the best written code can be awarded with a prize; students can be judged on the algorithms used. This enables every student to participate and perform at her favourite skill. ... It can be implemented in any functional programming language that supports some kind of windowing toolkit.

Teaching Functional Programming with Soccer-Fun (pdf)