# IO and Concurrency Programs must touch the world. They read files, open sockets, query databases, render pixels, and occasionally launch missiles. **Pure functions**, by definition, cannot do any of this. They map inputs to outputs, indifferent to the universe outside their arguments. And yet we write programs precisely to change that universe, to impose our will on entropy, to build something that persists after the process exits. This is the fundamental tension of typed functional programming, and **IO** is how we resolve it. The insight is to describe impure computations as pure values. An `IO String` is not a string obtained through **side effects**; it is a pure, inert description of a computation that, when executed by the runtime, will interact with the world and produce a string. The description itself is referentially transparent. You can pass it around, store it in data structures, combine it with other descriptions, all without anything actually happening. Only when the runtime interprets the description do effects occur. The effect is separated from the specification of the effect, and that separation is everything. When effects are explicit in types, the signature `readFile : FilePath → IO String` tells you something important: this function touches the filesystem. Compare this to a language where any function might secretly perform IO, where you cannot know without reading the implementation whether `getUserName()` is a pure lookup or a network call. The type becomes documentation that cannot lie. More than that, it becomes a constraint that tools can check. A function typed as pure cannot sneak in a database write. The compiler enforces the separation. Effects come in varieties. Observable effects change the world in ways the program can later detect: writing a file, then reading it back. Unobservable effects change the world but leave no trace the program can see: logging to stderr, incrementing a metrics counter, writing to `/dev/null`. Then there are effects with international consequences: the missile launch, the funds transfer, the irreversible deletion. Code that launches missiles should look different from code that formats strings. When effects are tracked in types, it does. The engineer reading the signature knows what they are dealing with. The engineer writing the code must confront, at every function boundary, whether this operation belongs in IO or whether it can remain pure. A bear foraging in the forest leaves tracks; a program touching the world should leave type signatures. This is engineering discipline: knowing the consequences of your logic and designing systems where those consequences are visible, reviewable, and constrained. This matters for the same reason everything in this series matters: we are building systems too complex to hold in our heads, increasingly written by machines that have no heads at all. Explicit effect tracking is not academic purity worship. It is engineering discipline for an era when the codebase is larger than any human can read and the authors include [entities that optimize for plausibility rather than correctness](./21_artificial_intelligence.md). The type signature is the contract. The contract is the only thing we can trust. ## IO Basics The IO monad represents computations that can perform side effects. All effectful operations live inside IO, and you sequence them using do notation. The "Hello, World!" of functional programming is not a string; it is `IO Unit`, a description of an action that, when run, will emit bytes to a file descriptor and return nothing interesting. The `Unit` return type is honest about its triviality: we did not call this function for its result but for its consequences. ```lean {{#include ../../src/ZeroToQED/IO.lean:io_basics}} ``` ## Pure Computations in IO Not everything in IO needs to be effectful. Pure computations can be lifted into IO when you need to mix them with effects. The `pure` function wraps a value in an IO that does nothing but return that value. This is not contamination; it is embedding. A pure value inside IO is like a diplomat with immunity: present in foreign territory but untouched by local laws. You can always extract the pure part because it never actually did anything. ```lean {{#include ../../src/ZeroToQED/IO.lean:io_pure}} ``` ## File Operations File operations live in the `IO.FS` namespace: read, write, append, delete, the usual POSIX inheritance. Files are where programs meet persistence, where the ephemeral computation leaves a mark that outlasts the process. The filesystem is the boundary between the volatile and the durable, between the RAM that vanishes when power fails and the spinning rust or flash cells that remember. Every configuration file, every log, every database is ultimately bytes on a filesystem, and the operations here are how you reach them. ```lean {{#include ../../src/ZeroToQED/IO.lean:file_io}} ``` ## Processing Lines Reading a file line by line is the fundamental pattern of Unix text processing, the reason `awk` and `sed` exist, the shape of a thousand shell pipelines. The newline character is civilization's oldest API, a contract that dates to the teletype and has outlived every attempt to replace it. In Lean, you get the same streaming capability with type safety and without the quoting nightmares that have spawned more security vulnerabilities than any other single source. ```lean {{#include ../../src/ZeroToQED/IO.lean:file_lines}} ``` ## Error Handling IO operations can fail. Files go missing, networks drop packets, disks fill up, permissions change, the NFS mount goes stale, the USB drive gets yanked mid-write. The universe is hostile to running programs, and error handling is how we cope with entropy's preference for chaos. Like a bear preparing for winter, a robust program anticipates scarcity: the resource that was there yesterday may not be there tomorrow. Lean provides try-catch blocks that should feel familiar to anyone who has written Java, Python, or JavaScript, except that here the error handling is explicit in the type. An IO action either succeeds or throws, and `try`/`catch` is how you intercept the failure before it propagates to somewhere you cannot recover. ```lean {{#include ../../src/ZeroToQED/IO.lean:error_handling}} ``` ## Mutable References Sometimes you need a mutable cell, a box you can read from and write to as the computation proceeds. `IO.Ref` provides this: a **reference** that lives in IO, supporting `get`, `set`, and `modify`. This is controlled mutation, explicit in the type system, not the invisible aliasing that makes imperative code a maze of spooky action at a distance. The reference is a value. You can see who has access to it. You can trace where it flows. The mutation is real, but the accounting is honest. ```lean {{#include ../../src/ZeroToQED/IO.lean:io_ref}} ``` ## Monad Transformers: ExceptT Real programs layer effects. You want IO for the filesystem, but you also want typed errors that propagate cleanly. **Monad transformers** stack these capabilities like geological strata, each layer adding something to the computation below. `ExceptT` wraps another monad and adds the ability to short-circuit with a typed error. The result is a computation that can both perform IO and fail with a specific error type, the signature making both capabilities explicit. The layering is architectural, not just convenient. The type tells you exactly what can go wrong and what side effects might occur. ```lean {{#include ../../src/ZeroToQED/IO.lean:except_t}} ``` ## Monad Transformers: ReaderT `ReaderT` provides access to a read-only environment, an implicit parameter that threads through your computation without cluttering every function signature. This is the dependency injection pattern done right: instead of global variables that any code can mutate, you have a typed environment that flows lexically through your program. Configuration, database connections, logger handles, the parameters that everything needs but nothing should own. The environment is read-only, which means you can reason about it. No function can secretly change the configuration and break something downstream. ```lean {{#include ../../src/ZeroToQED/IO.lean:reader_t}} ``` ## Running External Processes Lean can spawn external processes and capture their output, bridging the gap between the typed world inside your program and the untyped chaos of shell commands. This is where you call out to `git`, invoke compilers, run linters, orchestrate builds. The interface is necessarily stringly-typed at the boundary, but you can wrap it in whatever validation your domain requires. Just remember that every subprocess is a portal to undefined behavior: the external program can do anything, and your types cannot save you from what happens on the other side. ```lean {{#include ../../src/ZeroToQED/IO.lean:process_io}} ``` ## Environment Variables Environment variables are the original configuration mechanism, a key-value store that predates databases by decades. They are inherited from parent processes, invisible in your source code, and different on every machine. This is both their power and their peril. `PATH`, `HOME`, `USER`, the secret sauce that makes your program behave differently in development and production. Access them through IO because reading them is an effect: the same code will behave differently depending on what the shell exported before launch. ```lean {{#include ../../src/ZeroToQED/IO.lean:environment}} ``` ## The Discipline of Effects The history of programming is a history of discovering what we should not have been allowed to do. Unrestricted goto gave us spaghetti code; we constrained control flow with structured programming. Unrestricted memory access gave us buffer overflows; we constrained pointers with ownership and garbage collection. Unrestricted side effects gave us programs impossible to test, impossible to parallelize, impossible to reason about. We are still learning to constrain effects. Every constraint is a gift. When the type system refuses to let you perform IO in a pure function, it is saving you from bugs that would surface only in production, only under load, only on the third Tuesday of months with an R in them. The constraint is leverage. The IO monad is a template for how to think about the boundary between your program and the world. The world is messy, stateful, concurrent, and hostile. Your program can be clean, pure, sequential, and predictable. The boundary between them should be narrow, explicit, and scrutinized. That is engineering discipline for systems that must work when no one is watching. ## The Second Arc This concludes the programming arc. You can now write typed functions, define data structures, use type classes for abstraction, sequence effects with monads, and interact with the operating system. You have written FizzBuzz, parsed command-line arguments, read files, handled errors, and spawned processes. Congratulations, you are a Lean programmer. Time to become a Lean prover. Lean is both a programming language and a theorem prover. The same type system that checks your functions can verify mathematical claims. The same compiler that rejects type errors can reject invalid proofs. Everything you have learned carries forward, because in Lean, proofs are programs and propositions are types. This is not a metaphor. It is a mathematical theorem called the [Curry-Howard correspondence](./12_type_theory.md), and it means the skills you just built are directly applicable to theorem proving. You have already seen hints of this: [`Fin n`](./06_data_structures.md#fin) bundles a number with a proof it is in bounds; [subtypes](./06_data_structures.md#subtypes) attach predicates to values. These were not special cases but instances of the general pattern. Consider what you already know. You know that every expression has a type, and the type checker verifies that expressions have the types you claim. You know how to construct values: literals, function applications, pattern matching, recursion. You know that the compiler rejects programs that do not type-check. These facts carry over unchanged. A proposition is just a type. A proof is just a value of that type. When you prove \\(P \to Q\\), you are constructing a function from `P` to `Q`. When you prove \\(P \land Q\\), you are constructing a pair. When you prove \\(\forall n, P(n)\\), you are constructing a function that takes any `n` and returns a proof of `P n`. The vocabulary changes, but the mechanics are the same. The second arc introduces new tools for constructing these values. **Tactics** are commands that manipulate an incomplete proof, filling in pieces step by step. Where term-mode proof requires you to write the entire proof term at once, tactic-mode lets you work interactively: state a goal, apply a tactic, see what remains, repeat until nothing remains. The Infoview panel that showed you types and values now shows you goals and hypotheses. The tight feedback loop remains. You will also encounter new concepts. **Induction** is recursion wearing a different hat. **Case analysis** is pattern matching. **Proof by contradiction** is constructing a function from `\neg P` to `False`. The jargon can be intimidating, but the underlying structures are ones you already understand. When someone says "we proceed by induction on `n`," they mean "we define the proof recursively, with a base case for zero and a step case that assumes the result for `n` and proves it for `n + 1`." You have been writing recursive functions all along. What changes is the goal. In Arc I, you wrote programs to compute outputs from inputs. The type system ensured your functions were well-formed. In Arc II, you write proofs to establish that propositions are true. The type system ensures your proofs are valid. A proof is a program whose return type happens to be a logical statement rather than a data structure. The compiler verifying your proof is the same compiler that verified your FizzBuzz implementation. It just happens to be checking a different claim. This is the strange magic of dependent types. The wall between computation and logic dissolves. You can write a sorting function and prove it sorts. You can implement a parser and prove it handles all inputs. You can design a protocol and prove it never deadlocks. The same language, the same compiler, the same workflow. The boundary between "programming" and "proving" becomes a matter of which types you are constructing values for. The articles ahead cover: the foundations of proof in Lean, type theory and the Curry-Howard correspondence in depth, dependent types and their power, strategies for approaching proofs, a comprehensive tactics reference, and applications from classic mathematics to software verification. By the end, you will be proving theorems about the programs you write, and understanding why that matters. The transition may feel abrupt. Programming and mathematics have been taught as separate subjects for so long that their unification can seem like a category error. It is not. The historical accident is that they were separated. Lean reveals them as aspects of the same thing: constructing terms of specified types. What you learned in Arc I is directly applicable to Arc II. The rest is vocabulary. Let us begin.