Lessons

One command hides four layers of software and a set of standards that made them interchangeable. This lesson takes the stack apart, then asks the question the whole path has been building toward: given a shared kernel, how much is container isolation actually worth, and what has to be added before it is a security boundary.

Isolation is the point, and a container that can reach nothing and keep nothing is useless. This lesson covers how a network namespace is wired to the outside, why published ports and container-to-container traffic work completely differently, and where data has to live given that the writable layer disappears.

The kernel gives isolation for files already on the machine. The image format is what turned a directory tree into something you can build once, name by digest and run anywhere. This lesson covers layers and the union filesystem that stacks them, why the build cache behaves as it does, and the content addressing that makes it all work.

There is no container object in the Linux kernel, no container system call, and no container data structure. A container is an ordinary process started with several isolation features switched on at once. This lesson establishes what those features are, what the word actually names, and why the distinction changes how you reason about them.

Git's undo commands are notoriously confusing because they are usually memorised as recipes. Read against the object model they separate cleanly: each acts on a different one of the three places content lives. This lesson maps them, covers recovery from the accidents that feel unrecoverable, and states what genuinely cannot be undone.

Every operation so far moved a pointer. Merging is the first that has to decide something: two branches changed the same project and one result must come out. This lesson covers the three-way merge and the merge base it depends on, what a conflict actually is, and why rebase produces different commits rather than moving them.

Hashes are unusable by hand, so Git names them. A branch is not a copy of anything, not a directory, and not a container for commits: it is a forty-character file. Once that is clear, checkout, reset, detached HEAD and the reflog stop being separate concepts and become one operation on one kind of file.

Git is usually taught as a set of commands. Underneath it is a key-value store where the key is a hash of the content, and four object types built on that one idea. This lesson derives the hash by hand, shows what a commit actually contains, and explains why the design makes history tamper-evident.

Go is unusual for what it refuses to include. Errors are values, not exceptions. Interfaces are satisfied without declaring it. Formatting is not a choice. This lesson works through the omissions, the reasoning behind each, and the real costs, because every one of them trades expressiveness for something else.

Starting a goroutine is one keyword; stopping one is a design decision nothing forces you to make. A goroutine blocked forever is never collected and holds everything it references, which is the most common Go-specific bug. This lesson covers how leaks happen, the cancellation mechanism that prevents them, and how to detect the ones already there.

Cheap concurrency without a coordination primitive is a bug generator. Go's answer is a typed conduit that carries values between goroutines, from a 1978 idea: rather than protecting shared state with locks, pass ownership through a channel so there is no sharing to protect. This lesson builds channels, select, and where the model does not fit.

A thread costs enough that programs are architected around not having many. A goroutine costs little enough that the constraint disappears, which changes what designs are available. This lesson explains where the saving comes from, what the runtime scheduler does with them, and what the abundance does not fix.

The borrow checker rejects some correct programs, so Rust provides ways out: runtime-checked cells, reference counting, and unsafe blocks. This lesson covers what each escape hatch turns off, what it does not, and the encapsulation discipline that keeps a small unsafe core from voiding the guarantee for everything above it.

Rust did not add a concurrency safety mechanism. A data race requires aliasing plus mutation, which the borrow checker already forbids, so data races became compile errors as a side effect. This lesson shows how two marker traits extend that guarantee across threads, and what it still does not prevent.

Moving a value to read it is unusable, so ownership needs a way to lend. The lending rule is one line, and it is the reason Rust can guarantee no dangling references: you may have many readers or one writer, never both. This lesson builds that rule and the lifetimes that enforce it across function boundaries.

Every language must decide who frees memory and when. Rust answers with a rule enforced at compile time: each value has exactly one owner, and it is freed when that owner goes out of scope. This lesson builds the rule, shows what moving a value means, and explains what the approach buys and charges.

Two landmark systems carry machine-checked proofs of real code: a C compiler and an operating system kernel. Their published effort figures give the honest price of full verification, and their trusted computing bases show exactly what a proof still leaves unproved. This lesson uses both to decide where verification pays.

The third tradition supplies no invariants and writes no proofs. It builds the set of states a system can reach and checks the property against all of them, which is decidable when that set is finite. This lesson covers what it buys, the state explosion that limits it, and the techniques that made it usable anyway.

The other tradition does not prove a program correct after writing it. It designs a type that only correct programs inhabit, so the compiler's ordinary check is the proof. This lesson builds the correspondence between types and logic, shows what dependent types add, and covers the price the approach charges.

Testing samples inputs; a proof covers all of them. The machinery is a logic in which programs are statements about how they change what is true. This lesson builds Hoare triples, works a proof by hand, and identifies the one step that cannot be automated and is therefore where the work is.

Two different things can make a numerical answer inaccurate: the problem may amplify any input perturbation, or the algorithm may introduce its own. They are separate quantities, one belongs to the problem and one to the code, and only the second is fixable. This lesson separates them and shows what follows.

Equality fails on floats, and both standard replacements fail too: absolute tolerance breaks at scale, relative tolerance breaks near zero. This lesson works through why each fails, what the combined form actually does, and how to choose a tolerance from the problem rather than copying a magic constant.

Every operation is correctly rounded, yet results can be wrong in the first digit. The reason is that subtracting nearly equal numbers is exact and still catastrophic: it does not create error, it promotes error that was already there. This lesson builds that mechanism and the summation techniques that recover the lost accuracy.

Floating point is not a slightly inaccurate version of real numbers. It is a finite set of values, spaced logarithmically, with exact rules. This lesson builds the IEEE 754 layout, shows why 0.1 cannot be represented, and derives the one error bound that every later result depends on.