We develop at the gate level most of the schematics of a processor with superpipelining, delayed branch, forwarding, hardware interlock, speculative execution, caches, nested precise interrupts and out of order execution.
We prove the correctness of most constructions.

The foremost motivation for presenting mathematical correctness proofs is efficiency of teaching: computer architecture is complicated (unless one ignores crucial details) and the proper use of mathematics permits even the explanation of complicated things at a relaxed pace.

The second motivation is formal verification: our correctness proofs can be entered into and verified by interactive theorem provers.

This lecture will be in English!