Learn to build safety-critical systems in C.
Not "Hello World". Real kernels. Mathematical rigour. Zero dependencies.
"Don't learn to code. Learn to prove, then transcribe."
Most tutorials teach you to write code that seems to work.
This course teaches you to write code that provably works.
The method:
- Define the problem precisely
- Prove correctness mathematically
- Design structs that embody the proof
- Code (it writes itself)
- Test against the contracts
┌─────────────────────────────────────────────────────────────┐
│ THE APPROACH │
├─────────────────────────────────────────────────────────────┤
│ │
│ Problem ──► Math Model ──► Proof ──► Structs │
│ │ │
│ ▼ │
│ Verification ◄── Code │
│ │
└─────────────────────────────────────────────────────────────┘
Pulse — Heartbeat Liveness Monitor
A tiny, provably-correct state machine that answers: "Is this process alive?"
- 5 lessons from problem definition to hardened code
- ~200 lines of C with mathematical proofs
- Handles clock wrap, faults, and edge cases
- Zero dependencies beyond libc
More projects coming...
- Developers who want to understand why code works, not just that it works
- Systems programmers building safety-critical software
- Anyone tired of "it works on my machine" engineering
- Students who want to learn C the right way
- Basic C syntax (variables, functions, structs)
- Comfort with command line
- Willingness to think before coding
cd projects/pulse
make
./build/pulseThen start with Lesson 1: The Problem.
William Murray — 30 years UNIX systems engineering
- GitHub: @williamofai
- LinkedIn: William Murray
- Website: speytech.com
MIT — See LICENSE