Learn to build safety-critical systems in C.
Not "Hello World". Real kernels. Mathematical rigour. Zero dependencies.
"Math → Structs → Code"
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 mathematically
- Prove correctness formally
- Design structs that embody the proof
- Transcribe the math into C
- Test against the contracts
┌─────────────────────────────────────────────────────────────┐
│ THE APPROACH │
├─────────────────────────────────────────────────────────────┤
│ │
│ Problem ──► Math Model ──► Proof ──► Structs │
│ │ │
│ ▼ │
│ Verification ◄── Code │
│ │
└─────────────────────────────────────────────────────────────┘
| Module | Question | Role | Tests |
|---|---|---|---|
| Pulse | Does it exist? | Sensor | ✓ |
| Baseline | Is it normal? | Sensor | 18/18 |
| Timing | Is it regular? | Sensor | ✓ |
| Drift | Is it trending toward failure? | Sensor | 15/15 |
| Consensus | Which sensor to trust? | Judge | 17/17 |
| Pressure | How to handle overflow? | Buffer | 16/16 |
| Mode | What do we do about it? | Captain | 17/17 |
Plus: Integration Example — All modules working together.
┌─────────────────────────────────────────────────────────────────────┐
│ MODULE 7: MODE MANAGER │
│ "The Captain" │
│ Decides: What mode? What actions allowed? │
└─────────────────────────────────────────────────────────────────────┘
↑
┌─────────────────────────────────────────────────────────────────────┐
│ MODULE 6: PRESSURE │
│ "The Buffer" │
└─────────────────────────────────────────────────────────────────────┘
↑
┌─────────────────────────────────────────────────────────────────────┐
│ MODULE 5: CONSENSUS │
│ "The Judge" │
└─────────────────────────────────────────────────────────────────────┘
↑
┌───────────────────┼───────────────────┐
▼ ▼ ▼
┌─────────────────┐ ┌─────────────────┐ ┌─────────────────┐
│ CHANNEL 0 │ │ CHANNEL 1 │ │ CHANNEL 2 │
│ Pulse → Base │ │ Pulse → Base │ │ Pulse → Base │
│ → Timing │ │ → Timing │ │ → Timing │
│ → Drift │ │ → Drift │ │ → Drift │
│ "Sensors" │ │ "Sensors" │ │ "Sensors" │
└─────────────────┘ └─────────────────┘ └─────────────────┘
| Module | Question | Key Insight |
|---|---|---|
| Pulse | Is it alive? | Existence must be proven continuously |
| Baseline | Is it normal? | "Normal" must be learned, not assumed |
| Timing | Is it regular? | Jitter indicates system stress |
| Drift | Is it trending? | "Temperature is normal but rising too fast" |
Consensus — Triple Modular Redundancy voting.
"With THREE clocks, we can outvote the liar."
Pressure — Bounded queue with backpressure.
"Only bounded queues let you choose deliberately."
Mode — System orchestrator with permissions matrix.
"Sensors report. The Captain decides."
Every module is:
- Closed — No external dependencies at runtime
- Total — Handles all possible inputs
- Deterministic — Same inputs → Same outputs
- O(1) — Constant time, constant space
- Contract-defined — Behaviour is specified, not implied
# Clone
git clone https://github.com/williamofai/c-from-scratch.git
cd c-from-scratch
# Try any module
cd projects/pulse
make && make test && make demo
# Or run the full integration
cd projects/integration
make runStart with Pulse Lesson 1: The Problem.
See SPEC.md for the complete framework specification:
- Core principles
- Module structure
- Contract definitions
- Composition rules
- Certification alignment (DO-178C, IEC 62304, ISO 26262)
- Developers building safety-critical software
- Systems programmers who want provable correctness
- Students learning C the rigorous way
- Anyone tired of "it works on my machine"
- Basic C syntax (variables, functions, structs)
- Comfort with command line
- Willingness to think before coding
William Murray — 30 years UNIX systems engineering
- GitHub: @williamofai
- LinkedIn: William Murray
- Website: speytech.com
MIT — See LICENSE
"Sensors report. The Captain decides."