An introduction to the mathematical underpinnings of reliable software, using the Software Foundations textbook series. Topics include functional programming, logic, program equivalence, and Lean-checked proof.