编程文化与语言设计的历史

需积分: 9 34 浏览量更新于2024-07-15 收藏 935KB PDF 举报

"这篇论文探讨了编程语言设计的文化背景，提出了编程文化的概念，将编程文化分为黑客文化、工程文化、管理文化和数学文化四个主要类别，并通过历史线索分析这些文化如何影响编程语言的设计和发展。" 在编程领域，语言设计并非孤立进行，而是与更广泛的社会技术环境紧密相关。"Culture of Programming" 这篇论文揭示了编程语言背后的社会-技术环境，其目的是深入理解编程的历史并以整体视角看待其演变。论文引入了“编程文化”的概念，这个概念代表了对编程的独特看法。首先，文章提到了四种主要的编程文化： 1. **黑客文化**：源自自由软件和开源运动，强调创新、自由以及技术熟练程度。这种文化推动了诸如Linux和Git等项目的发展。 2. **工程文化**：注重实用性和可维护性，强调软件构建的系统性和规范性，如C++和Java等语言体现了这一理念。 3. **管理文化**：关注效率和成本效益，倾向于采用标准化流程和工具，例如敏捷开发方法和企业级Java框架。 4. **数学文化**：强调逻辑严谨和形式化，推动了类型系统的演进，例如函数式编程语言Haskell和Lambda演算。为了探究这些文化如何相互作用并影响编程语言设计，论文通过四部分历史分析展开讨论： 1. **数学化编程**：从早期的图灵机到现代的抽象数据类型和算法，数学在编程中的应用加深了我们对计算的理解。 2. **类型系统的发展**：从静态类型到动态类型，再到类型推断，类型系统在确保程序正确性和提升开发效率方面扮演了关键角色。 3. **复杂软件系统的界限**：讨论了如诺伊曼的停机问题和哥德尔的不完备定理，它们揭示了复杂系统内在的局限性，影响了软件架构和设计原则。 4. **提高软件可靠性的方法**：包括错误检测、测试自动化、形式验证等，这些方法帮助现代软件达到可接受的可靠性水平。通过以上分析，论文试图构建一个连贯的框架，以连接各个编程语言的历史点，从而增进我们对编程文化及其对编程语言发展影响的整体理解。这对于我们理解编程语言设计的动机、选择和趋势具有重要意义，也为未来编程语言的研究和设计提供了历史和理论的参考。

Cultures of programming :13

the preceding sentences in the sequence by a rule of inference.”[Wikipedia contributors 2018] The

idealised view of mathematical proof is often based on this notion from formal logic. In practice,

proofs that mathematicians work with are quite dierent. They are written in a mix of natural and

formal language and they are written to convince another, adequately qualied, colleague that a

theorem holds, i.e. that a formal logical proof could be constructed.

Mathematical proofs are central objects of mathematical practice. They are taught at universities,

shared with colleagues and discussed in whiteboard sessions where mathematicians marvel at the

elegance of a proof and clever tricks that make it work. They almost never bother fully expanding

the proof to a proof as understood in formal logic.

In contrast, proofs of program correctness are bound to be secondary. The main reason for the

existence of a computer program is to run it. Proofs do not exist as main objects of knowledge,

but merely as certications that programs match their specications. This also explains some

of the dierences in how the two communities treat mechanised proofs. On one hand, many

mathematicians remain cautious about the use of computer in proofs [Gold and Simons 2008].

On the other hand, the idea that correctness proofs should be checked by a computer has been

proposed as early as 1962 by McCarthy [[n. d.]b] and has since become a main-stream method in

computer science.

In 1977, De Millo, Lipton and Perlis pointed out the dierence between proofs in mathematics and

computer science in a paper “Social processes and proofs of theorems and programs” [De Millo et al

1979], rst published in the ACM Symposium on Principles of Programming Languages (POPL)

and later in the Communications of the ACM. The paper triggered a controversy and was equally

labeled as “Marvelous, marvelous, marvelous!” and as “a political pamphlet from the Middle Ages”

[MacKenzie 2001, p.197].

According to De Millo et al., mathematical proofs encompass a rich structure of social processes

that determine whether mathematicians feel condent about a proof. Contrary to what its name

suggests, a proof is just one step in the direction of condence, but that is how actual mathematicians

construct actual mathematics. In other words, social processes are what gives mathematicians

condence in their proofs. The same social processes do not exist in computer science for proofs of

correctness and so they do not warrant the same condence.

De Millo et al. focused merely on the condence that we can have in the correctness of programs,

but the lack of social processes typical to mathematics could be even more signicant. As illustrated

by Lakatos et al

[1976], the attempts to produce a proof and refutations of earlier imperfect proofs

is what builds mathematical knowledge. A failed attempt to construct a proof lets us nd issues

with our denitions and theorems and encourages us to revise those. If we treat proofs merely

as certications, as computer scientists might, we lose an invaluable force that shapes the our

knowledge.

It is dicult to trace the direct eect that the De Millo et al. paper had on computer science.

As noted by MacKenzie [2004], the controversies triggered by the paper likely contributed to the

decrease of funding for formal verication, especially from the US military. However, many further

developments around program correctness address the issues raised by De Millo et al., even if they

are not a direct response to the debate triggered by their paper. Two approaches that we discuss

next reect two sides of the mathematical culture.

2.2 Mechanistic and intuitionalist culture of proving

The lack of social processes in proofs of programs can be addressed in two ways, depending on

who do we want to convince about program correctness. If we want to convince a human that

a program is correct, we need social processes, though not necessarily exactly the same as the

ones that mathematics has. If we want to convince a computer that a program is correct, we need

, Vol. 1, No. 1, Article . Publication date: January 2019.

:14 Tomas Petricek

to accept that program correctness proofs are of a dierent epistemological nature. For example,

mechanised proofs are perhaps better seen as technological artifacts [Turner and Angius 2017].

These two approaches can be seen as two sides of the mathematical culture of programming and

we will refer to them as the mechanist culture and the intuitionalist culture.

The split between the mechanist culture and the intuitionalist culture can be traced (at least) to

the birth of articial intelligence and the rst use of computers for automated theorem proving in

1950s. The Logic Theory Machine designed by Newell and Simon (which would eventually prove

38 of the rst 52 theorems in Principia Mathematica) captured heuristic rules that humans use and

was designed to understand how human beings reason. The work aimed at human understanding

and the prover later produced new proofs, regarded as elegant by human readers. In contrast,

methods advocated by logicians such as Wang [1960] used exhaustive search methods that were

inscrutinizable, but were able to prove all of the 52 theorems much faster than the method of Newell

and Simon [MacKenzie 2001, p.73]. As in the context of program correctness later, the proponents

of the intuitionalist culture such as Newell and Simon focused on human understanding while

Wang and other advocates of the mechanist culture focused on using computers in a way that is

not accessible to humans.

The cleanroom software engineering methodology, developed by Dyer and Mills [[n. d.]] com-

bines the intuitionalist mathematical culture, with its focus on convincing humans via social

processes, with a managerial culture that shifts focus from individuals to organizations. The

methodology proposes “a technical and organizational approach to software development with

certiable reliability”. It aims to prevent defects, as opposed to debugging them later, by using

software specications and rigorous proof. However, the goal of a proof was to convince fellow

team members that the program was correct. This was done through a social process akin to modern

code reviews. The social processes that were lacking in proofs of program correctness are restored

through the business organization, which recognized that additional time spent while reviewing

(perhaps tedious) conformance to the specication will save time later. The process of proving

in the cleanroom methodology is fundamentally human. “It is obvious” is an acceptable proof if

everyone agrees. It does not provide an absolute certainty, but when practiced well, it does notably

decrease the defect rate [MacKenzie 2004].

The proponents of the mechanist culture were not satised with proofs checked by humans

and argued, as McCarthy did in 1962 that proofs of program correctness should, themselves, be

checked by a computer program. Unlike the early work in AI on automatic theorem proving, which

was able to obtain some, albeit limited, results automatically, verication of non-trivial programs

required (and still requires) human input. The computer thus “does not act as an oracle that certies

bewildering arguments for inscrutable reasons but as an implacable skeptic that insists on all

assumptions being stated and all claims justied.” [MacKenzie 2004, p.272]

The rst tool that was born from the mechanistic mathematical culture was the LCF theorem

prover, introduced by Milner [1972]. The work on LCF was motivated by program correctness and,

more specically, compiler correctness proof [Milner 1979]. To simplify construction of LCF proofs,

Milner’s group developed a meta-language (ML) which could be used to develop proof procedures.

Those were, in turn, checked to be correct by the ML type checker. This powerful combination

gave rise to a family of interactive theorem provers that are still popular today (HOL, Coq, Nuprl

[Constable 1986; Coquand and Huet 1988; Gordon 1988]) that directly follow in the mechanist

mathematical tradition. However, the ideas developed as part of the ML metalanguage soon took a

new form as a stand-alone programming language.

Mechanized proofs developed using LCF and similar tools are no longer the complex human

constructs that mathematicians know as proofs that require social processes for their verication.

Instead, they are a computer representation of a sequences of propositions where a prover program

, Vol. 1, No. 1, Article . Publication date: January 2019.

Cultures of programming :15

can derive each proposition from earlier sentences, axioms or assumptions. This notion is close to

the notion of proof in logic, with the caveat that we are now talking about computer representations.

2.3 Theorems and formal specifications of ALGOL

The critique of De Millo et al. focused on the notion of proof. A proof of program correctness is

not the same kind of proof as a proof in mathematics. However, this is not the only discrepancy.

The theorems proved by proponents of the mathematical programming culture are also quite

dierent notions than the theorems proved by mathematicians. In programming, the structure

of the theorems is mainly shaped by the programs they talk about and the programs, in turn,

are shaped by the aim of building software that can be run to achieve some task. In contrast,

mathematical theorems are shaped by the proofs, counter-examples and the preferences of the

mathematical community which strives for simplicity and elegance. As a result, the specications

that computer scientists work with (and hence also the theorems about them) are either extremely

complex or signicantly simplied and, quite often, both of these.

The two mathematical sub-cultures can, again, help us understand how specications are written.

On one hand, the aims of the mechanist culture are to provide specications that can be, at least in

principle, checked automatically against an actual implementation. This requires that it is written

in a fully formal language and that it is as complete as possible. On the other hand, the aims of

the intuitionist culture are to explain key aspects of the program behaviour to a human. For this

reason, the specication can use natural language where appropriate and does not necessarily have

to cover everything. It can focus on a subset of the program that is expected to be tricky and cannot

be skipped as “obvious”.

An illuminating example is provided by the various attempts of formally dening the ALGOL

60 programming language that have been documented in detail by Jones and Astarte [2016]. The

Revised report on the algorithmic language ALGOL 60 [Backus et al

1963] denes the syntax of

ALGOL mathematically using the BNF notation, but the semantics of the language is dened in

carefully-crafted English language. The report was produced under the inuence of many cultures,

but the main focus was to explain ALGOL 60 to humans including programmers working in the

industry, as well as mathematicians.

McCarthy [[n. d.]a] followed his aim of dening a mathematical science of computation and

dened a formal mathematical semantics of a subset of ALGOL named Microalgol. McCarthy

“advocates an extension of [his] technique as a general way of describing programming languages,”

but keeps the language to a trivial subset (including goto, but omitting many other aspects of real

ALGOL). Similarly, in his An axiomatic basis for computer programming, Hoare [1969] chooses to

study properties of a very simple language (with assignment and iteration, but without goto) Hoare

notes that there “does not appear to be any great diculty in dealing with [most other aspects of

ALGOL]” with the exception of jumps. He optimistically claims that “the practice of supplying

proofs for nontrivial programs will (...) not be easy, [but] the practical advantages of program

proving will eventually outweigh the diculties.”

Providing semantics for the full ALGOL 60 language was signicantly more work. The operational

semantics given by Lauer [1968] from the Vienna IBM laboratory is 67 pages and provided a

motivation for follow-up work aiming to give simpler semantics, including simpler operational

semantics Allen et al

[1972] and Vienna denotational semantics [Henhapl and Jones 1978] which

is “simple enough to t a book chapter.” [Jones and Astarte 2016] The dierent sub-cultures can,

perhaps, be seen in the notations used. The Oxford denotational semantics [Mosses 1974] uses

mathematical symbols and is thus written to explain ALGOL 60 to a mathematician whereas the

Vienna denotational semantics [Henhapl and Jones 1978] is written in the VDM language and is

more accessible for mechanical processing, although the tool support only provided basic checking.

, Vol. 1, No. 1, Article . Publication date: January 2019.

剩余74页未读，继续阅读

gonearewe

粉丝: 0
资源: 2

编程文化与语言设计的历史

The Art of Unix Programming

Literate programming, Why

unix编程艺术（英文版，The Art Of Unix Programming）

Robert Galanakis - Practical Maya Programming with Python

【In-depth Understanding of MATLAB Spectrum Analysis】: The Mysteries of FFT and IFFT

MATLAB Pricing and Technological Advancement Correlation: The Impact of Technological Innovation on ...

c语言实现图片转化为 ASCII 图.zip

【路径规划】模拟退火算法结合LNS求解车辆路径规划问题【含Matlab源码 2333期】.zip

Java毕业设计/课程设计Springboot+Vue开发的反诈视频宣传系统

c语言商品销售系统源码.zip

最新资源