Notes to Computer Science Freshmen from the Future

There is a major programming shift happening. In the last few years there has been major advances in program proof technology. The magic words are the "Curry-Howard Isomorphism". Having lived through structured programming, CLU modules, Pascal strong typing, Smalltalk object-oriented programming, distributed programming, functional programming, and other such trends I can tell you that proving programs correct is "the next big thing".

I predict that within 5 years you'll be expected to write proven programs. Test-Driven Development (TDD) is toast. It doesn't work and it wastes time. Prove your program and generate code from your proof. That works today. Why aren't you using it?

Your car will be "brake by wire" where the brakes are applied by computer after you step on the brake pedal (if you have one). You REALLY want to PROVE that the brakes will be applied within 1ms. Your life depends on it.