One line of code crashed the Ariane 5. One line killed patients with the Therac-25. One line cost Knight Capital $440 million in 45 minutes.
Different domains. Same cause: software that failed silently until it was too late.
This book teaches you to write C that fails loudly, early, and for a reason - or not at all.
The approach comes from aerospace and medical device certification, where "it works on my machine" isn't acceptable - and undefined behaviour isn't a learning experience, it's a liability.
You'll learn to:
- Define correctness before a single line is written
- Design data structures that make invalid states unrepresentable
- Write code as a literal transcription of proven contracts - not guesswork
Test behaviour, not hope
What You'll Build
11 chapters take you from fixed-width integers to a complete, provable state machine - each concept grounded in real-world failures and how to prevent them.
The progression:
1. The Philosophy - why proving first changes everything
2. Fixed-Width Integers - why `int` is a trap
3. Booleans and Decision Logic - contracts that catch bugs at compile time
4. Arrays - bounds you can prove
5. Strings - buffer safety without the mystery
6. Structures - data design that prevents invalid states
7. Pointers - ownership made explicit
8. Functions - contracts as code
9. State Machines - complexity you can reason about
10. Capstone: Tic-Tac-Toe - prove correctness before writing game logic
11. Path to Production - from learning to shipping
Plus four appendices: Development Setup, Contracts Quick Reference, Fixed-Width Types Reference, and Common Undefined Behaviours.
Who This Is For
- Self-taught developers wanting rigorous foundations
- Engineers moving into embedded or safety-critical domains
- Anyone tired of debugging code that "should" work
- Students who want to understand why not just how
No prior C experience required. Just a willingness to think before you type.
What Makes This Different
Most C books teach syntax. This one teaches thinking.
You'll spend less time memorising rules - and more time eliminating entire classes of bugs before they exist.
The methodology - MATH → STRUCT → CODE → TEST - is how certified systems are actually built. Before writing a single line, you define the mathematical properties your code must satisfy. Then design structures that enforce them. Then implement. Then verify against the original proof.
Not because you'll build a pacemaker, but because the discipline makes you a better programmer.
By the end of this book, you won't just write C - you'll reason about it.
