computer-science

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.

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.

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.

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.

Counting distinct items exactly needs memory proportional to the count. HyperLogLog answers the same question in a fixed twelve kilobytes, for cardinalities into the billions, by measuring an improbable event rather than storing anything. This lesson builds that idea from the leading-zeros intuition up.

A Bloom filter answers set membership using a bit array and a handful of hash functions, with no items stored anywhere. This lesson builds it, derives the sizing formula that trades memory against false positives, explains exactly why deletion is impossible, and covers the variants that buy it back.

Answering set questions exactly costs memory proportional to the data, which fails once the data does not fit. Probabilistic data structures accept a quantified error in exchange for memory that stays constant. This lesson establishes what that trade buys, and why the shape of the error matters more than its size.

The two renderer architectures are not competing implementations of the same idea. One sorts fragments for a single viewpoint, the other searches for a hit along an arbitrary ray. Reading them that way explains which effects are cheap in each, why production renderers combine them, and what a hybrid actually buys.

Rice's theorem closes every interesting question a type checker, linter or verifier wants to answer, yet those tools exist and work. They work by choosing which way to be wrong. This lesson covers the sound and unsound bargains, the provable approximation in pointer analysis, and the option of leaving Turing completeness behind on purpose.

Once memory stops being the constraint, a different kind of limit appears. No program can decide whether an arbitrary program halts, and the proof fits in eight lines. This lesson builds that argument, separates deciding from merely recognising, and shows how one impossibility result propagates to every other question worth asking.

Finite memory fails on anything that must be counted, so add memory and watch what each purchase buys. A stack buys nesting and nothing more. An unbounded tape buys everything, and two entirely different formalisms invented in the same year turn out to buy exactly the same thing.