Position Paper: Practical Foundations for Programming Languages

摘要

A program is a form of expression that conveys an idea, much as does a proof in mathematics. But whereas proofs have only a static significance, as a form of communication, programs also have a dynamic significance,as commands to be executed by a machine. This places very strong demands on the programmer to explain herself so precisely and rigorously that a program can be run on a computer, while at the same time so crisply and elegantly that a human would be able and willing to understand her.