Programming Languages

Every programming language embeds a philosophy — a set of beliefs about what matters, what can be trusted, and where complexity should live. This section traces how those philosophies play out in practice, from C's faith that the programmer knows best (which gave us undefined behavior and Spectre) to Rust's faith that the type system knows best (which gave us memory safety and fight-with-the-compiler sessions). The deepest thread is the Curry-Howard Correspondence: the discovery that types are propositions, programs are proofs, and your compiler has been doing philosophy whether you asked it to or not.

The Design Axis

Language Design Philosophy frames the central tension: worse is better vs. the right thing. C and Unix won by being 50% right and running everywhere. Lisp lost by being beautiful and running nowhere. The Lisp Curse — that powerful languages fragment because every programmer becomes an island — is the evil twin of worse-is-better. Erlang's let-it-crash philosophy represents an orthogonal axis entirely: don't prevent failure, make failure a building material.

The seven ur-language families (ALGOL, Lisp, ML, Self, Forth, APL, Prolog) each represent a genuinely different way of thinking about computation. Most programmers only know the ALGOL family. Learning a second family — Forth's stack discipline, Logic Programming's relational bidirectionality, ML's type-driven design — changes how you think even when you're writing Python.

The Type Theory Spine

The section's intellectual backbone runs from Curry-Howard through Substructural Type Systems to Pointer Provenance and Recursion Schemes. The key insight: for every logic system, there's a type system, and vice versa. Classical logic gives unrestricted types. Intuitionistic logic gives constructive types (Haskell). Affine logic gives Rust's ownership. Linear logic gives Forth's stack discipline — Baker's 1993 paper showed that Forth's dup and drop are literally the contraction and weakening operators of substructural logic, anticipating Rust by two decades.

Proof assistants like Lean push this to its limit: Scholze's Liquid Tensor Experiment verified cutting-edge mathematics mechanically, and the verification process actually improved the proof. The convergence of compiler correctness and proof assistants suggests a future where verified compilation is derived from verified interpretation through reflective towers — write the interpreter, collapse it into a compiler, and the verification follows.

The C Problem

Three articles form a triangle of devastation around C's legacy. Undefined Behavior shows how the optimization-through-UB contract creates security vulnerabilities that the programmer cannot predict. The C Abstract Machine shows that C hasn't been "close to the metal" since the PDP-11, and the heroic effort to maintain the illusion is the direct cause of Spectre. Pointer Provenance shows that even the concept of "what a pointer is" is under-defined in ways that cause real miscompilations. Together they argue that C's abstract machine is not just obsolete but actively harmful — a PDP-11 fiction that hardware architects spend billions of transistors maintaining.

Compiler Correctness offers the constructive response: CompCert proved that verified compilation is practical, and random testing found zero optimizer bugs in its verified core while finding hundreds in GCC and LLVM. Program Synthesis suggests that SAT-based superoptimizers could eventually replace hand-written optimization passes, producing correct-by-construction transformations.

Liveness and Feedback

Immediate Feedback and Liveness In Programming form a two-part argument that the way we've been writing software since the 1950s — text files, compilation, observation, iteration — is fundamentally broken. Bret Victor's demos showed that mapping time to space and eliminating delay between intention and observation enables qualitatively different creative processes. Dynamicland pushed this into physical space. The demoscene connection is worth noting: Shadertoy is the accidental realization of Victor's principle for graphics programming, providing immediate feedback that drove the development of SDF techniques that eventually entered production engines.

Trust and Bootstrapping

Compiler Bootstrapping asks where the chain of trust begins — and connects to Supply Chain Trust and Thompson's Trusting Trust attack. The Bootstrappable Builds project starts from a 512-byte seed; SectorC fits a C compiler in a boot sector; Zig uses WebAssembly as a portable bootstrap format. Each approach represents a different answer to the question: how small does the trust kernel need to be?

What Connects Outward

The PL section connects to AI through Mechanistic Interpretability (transformers have a functional anatomy discoverable through the same circuit-analysis vocabulary), to philosophy of mind through Language And Thought (programming languages are cognitive technologies that reshape what's computationally tractable for the programmer), and to economics through Inadequate Equilibria (the worse-is-better dynamic is a coordination failure where individually rational language choices produce collectively suboptimal ecosystems). Concurrency Models bridges to hardware architecture: Erlang's message-passing model, if taken seriously, would let hardware designers shed the enormous complexity of cache coherency protocols — the same point that the C abstract machine article makes from the other direction.