The Limits of Type Systems

综合编程 2013-09-03

E.W.Dijkstra Archive: The Humble Programmer (EWD 340)

Argument three is based on the constructive approach to the problem of program correctness. Today a usual technique is to make a program and then to test it. But: program testing can be a very effective way to show the presence of bugs, but is hopelessly inadequate for showing their absence. The only effective way to raise the confidence level of a program significantly is to give a convincing proof of its correctness. But one should not first make the program and then prove its correctness, because then the requirement of providing the proof would only increase the poor programmer’s burden. On the contrary: the programmer should let correctness proof and program grow hand in hand. Argument three is essentially based on the following observation. If one first asks oneself what the structure of a convincing proof would be and, having found this, then constructs a program satisfying this proof’s requirements, then these correctness concerns turn out to be a very effective heuristic guidance. By definition this approach is only applicable when we restrict ourselves to intellectually manageable programs, but it provides us with effective means for finding a satisfactory one among these.

Essentially what Dijkstra is advocating here is what the approach the most advanced type theories are striving for. They aim to allow the programmer to specify in the type system (a proof system) important semantic invariants of the application. The type system is constructed in such a way the program is only well typed if the specified invariants hold. The hope of the type theorists is that with a sufficiently powerful type (proof) system most if the not all properties one cares to prove are in fact provable (for certain programs).

The difficulty for the practicing programmer is most type systems are not nearly powerful enough to specify properties which are actually interesting. This leaves the programmer doing essentially the proof equivalent of book keeping with no benefit. I should distinguish here between dynamically checked types (properties) and statically checked types. Dynamically checked, that is at run time, are always enormously helpful to the programmer because they provide runtime safety. However, statically checked types can be overly burdensome if they require lots of book keeping without sufficiently powerful proofs.

Unfortunately, for a wide variety of statically checked programming languages the available proofs are uninteresting and the burden is high. This is the challenge to the Dijkstra-ist.

您可能感兴趣的

CodeSOD: Attack of the “i” Creatures “ Mrs S ” works for a large software vendor. This vendor has a tendency to quickly increase staffing to hit arbitrary release targets, and thus re...
The best Easter Egg you ever did leave Where I work, a developer left an Easter Egg long ago where if you came to our ERP self service dashboard by way of 302 and had an expired SSO cookie,...
vn.py发布v1.7.1 – CTA策略模块升级版 前后忙活了两个月,终于算是完成发布了v1.7.1的版本。这次新版本主要针对的是CTA策略相关的功能,按照几个主要的方向来介绍下。 交易委托的开平仓自动转化功能 之前使用VnTrader来跑CTA交易策略,下单开平仓方面有两个让用户比较头疼的问题: 上期所合...
CPAL-1.0 开源许可证说明 CPAL-1.0 1.定义 1.0.1 “商业使用”是指发布或者以其他方式使第三方可以获得全部代码。 1.1 “贡献者”是指编写出代码或者对于代码的实质修改有贡献的各个实体。 1.2 “贡献者版本”是指原始代码,贡献者所使用的有过实质修改的源代码,以及仅由该贡献者所作...
Simplistic programming is underrated I was a nerdy kid who liked to spend a lot of time reading. Back then, we did not have the Internet, we could not even imagine it… so I ended up readi...