As one digs deeper into distributed systems, Lamport's writing keeps popping up. Below is a transcript of the last few slides in the video lecture.

[starting@28:30]

The fundamental problem facing computer engineers is complexity.

Good engineering means making systems as simple as possible.

The math needed to describe computer systems is simple.

Programming languages are complicated.

You don't achieve simplicity by thinking in terms of complicated languages.

Simplicity requires thinking abstractly before implementing.

This means thinking mathematically before writing any code.

TLA+ teaches how to think mathematically, but few engineers are willing to try.

They must overcome years of "brain washing" that began with their computer science education.

Mathematical thinking must be taught in universities.

I believe I know what students should learn:

  * Understanding a system as a state machine
  * Describing a state machine mathematically with an initial predicate and next-state relation.
  * Thinking of implementation as substitution.

Can anyone help explain what Lamport meant by "implementation as substitution"?