Stanford Seminar - Programming Should Be More Than Coding

This seminar argues that programming involves specifying what a program should do and how it should do it, in addition to coding. It introduces mathematical models, behavioral and formal specifications, TLA+, and their use in reasoning about algorithms and concurrent systems.

Syllabus

Introduction.
The 3 Tasks of Programming.
A Really Easy Problem.
How Can We Think More Clearly?.
Models versus Reality.
Computer Science.
What's a Program?.
Task 1: Specifying What the Program Does.
Our Example: A GCD Program.
Reality versus Model.
Limitations of the Function Model.
The Standard Behavioral Model.
Task 2 for Euclid's Algorithm.
The Complete Task 2 Specification.
What About Formal Specs?.
The Language: TLA.
The Problem with TLA.
The XBox 360 Memory System.
Why not a formal spec?.
What is Typical About This Spec.
What is Not Typical About This Spec.
What code should you specify?.
What should you specify about the code?.
How do you learn to write specs?.
How do you learn to write formal specs?.
How do you connect the spec to the code?.
What about coding?.