ILLOGICAL ENGINEERS
summary
Argues that much of modern practice — TDD, agile iterations, microservices patterns — is already documented back to the 1950s–1968 NATO discussions, then makes the case that stronger type systems and the Curry Howard correspondence let compilers catch real bugs (examples: forbidding cross-type equality, deriving semigroup instances to merge nested maps/options, small proof-driven implementations). Notes limits: Gödel incompleteness prevents a language from proving its own compiler, cites Agda and Coq and a new GitHub library Carey Howard that auto-generates implementations, and mentions Dr Kunth’s $3,372,548 bet.
AI-written summary · about
chapters (7)
- 0:00Start
- 8:13What Does It Mean To Be a Software Engineer
- 10:27Type System
- 13:45Carey Howard Correspondence
- 14:45Constructive Logic
- 20:05Russell and Whitehead
- 21:03Incompleteness Theorem
related talks
45mTDD, as in Type-Directed Development
58mKeynote: Why Functional Programming Matters
42mProgramming with Math
41mThe Dialectics of Type-Level Programming
41mChoosing Your Next Programming Language
01h 34mFormal Logic Undressed
28mLanguage Support for Property-Based Testing
34mHow I learned to stop worrying and love Functional Design