If you're a software developer with AI-induced depression, you should know that we're entering a golden age of programming. Lean is the cure. Types as specifications Any type system expresses some properties — even int vs string rules out a class of errors. Richer type systems express richer properties: generics constrain relationships between types, linear types track resource ownership, refinement types attach predicates to base types. But dependent types go further: types can depend on values, which makes the type language expressive enough to state arbitrary logical propositions. Not just "this is a list" but "this is a list of length n." Not just "this function returns a list" but "this function returns a list and here is a machine-checked proof that it is sorted." This is not speculative. This is Lean 4 today. The theoretical foundation is the Curry-Howard correspondence: types are propositions, and programs are proofs. A function of type A → B is not merely a piece of code that transforms A into B — it is a constructive proof that "if A, then B." When one writes List α → SortedList α, one is simultaneously defining a function and stating a theorem: "for every list, there exists a sorted version, and here is the evidence." The compiler does not merely check that the code runs — it checks that the proof is valid. The thesis follows directly: if the specification can be expressed as a type, the compiler becomes the verifier. The AI can produce whatever implementation it wants — insertion sort, merge sort, something entirely novel — and the compiler will reject it unless it comes with a valid proof that the output satisfies the specification. The proof is the guarantee. There is good reason to believe we are entering a golden age of type-driven development. Not despite AI, but because of it. AI is effective at generating code and filling in proof obligations. Humans are effective at stating what they want. Dependent types are the bridge. ngrislain.github.io/projects…