Types in Programming Languages, Between Modelling, Abstraction, and Correctness: Extended Abstract

摘要

The history of computer science is innervated by the continuous tension between formal beauty and technological effectiveness. Types in programming languages are an evident example of this dialectics. They are introduced for a better verification of the correctness of programs, and yet-contrary to mathematical logic-they must be experienced by the working programmer as an enabling feature, allowing for simpler writing of programs.