A Book Written in Types
PDF

Chapter 1

Machine and program

Take “machine” in the abstract sense – a transformation of input into output, not gears – and the distinction between machine and program dissolves entirely; the universal Turing machine makes that vivid. The chapter argues that the distinction survives in practice for two reasons only, economics and culture: physical machines cannot be built as cheaply as digital ones, and we doubled down on the von Neumann model, which builds the split into the architecture and makes state and location first-class. The lambda calculus is the road not taken. The languages descended from Algol and C are not at fault; they are honest reflections of that machine. That no language names time and space first-class is framing here, not thesis, and the industry’s interchangeable use of code, program, software and application is treated as a symptom of the same unfinished business.