对可计算性的分析是最高级的智力成就，也是一种历史的好奇心。在实际应用的计算机建立起来的许多年前，才华横溢的数学家们发现了描述计算能力和极限的某些特征。这些结论通常被用来陈述计算能够解决何种问题，但是这种标准的阐释是错误的。虽然关于计算的计算仅仅局限于理论，实际上这些限制并不能阻止实用和重要的计算分析。

    停机问题也许是可计算性研究中最基本的理论。可计算性对每一名计算机科学的学生来说都不啻于一块瑰丽的智慧宝石和一条习惯的必由之路。这是一个证明过于朴素的简单陈述。

    停机问题表明，没有办法推测一个特定输入的程序会不会永久循环或者最终得出结果并停止。如果你曾经坐在一台空白的计算机屏幕前，凝视并考虑计算机会不会再次对你做出反应，那么你会发现以下这种计算将是多么有益——中断当前的处理，询问计算机究竟能不能完成。如果计算机说不，那就可以取消这次计算，转身做一些更有帮助的事情。停机问题的解决方案实际上就这么简单。

    但是，停机问题并没有解决方案，这一点很容易用矛盾来证明。如果你已经忘记了如何用矛盾来证明，请遵循如下方式：如果你假设了一个命题，并且这个命题导致了矛盾，那么该命题一定是错误的。一个协调的逻辑系统不允许模糊的存在。每一个陈述只能是正确的或者是错误的，不可能二者兼有。

    因此，为了证明停机问题是不可能解决的，让我们先假设它可以解决：假定对于每一个程序，我能够估算出一个给定输入的程序是否最终会停止，完成计算并返回运行结果，而不是永久循环。

    既然程序可以利用其它的程序，那么我现在写一个奇特的程序：如果它的输入是一个停止于输入的程序，这个新的程序会永久循环。

    现在考虑新程序本身的应用。如果它停止，那就必须永久循环。如果它永久循环，那就必须停止。由于没有程序可以同时永久循环和停止，这就是一个矛盾。

    所以，假设停机问题可以解决是错误的：停机问题是不可计算的。

    如果你对这个证明感到疑惑，也许是因为你思索得太深入――或者也许你被一个关于可计算性的格外晦涩的讲演所吓倒。假定能够解决停机问题会马上产生矛盾，因此我们不可能具备那种能力。

    而且更糟的是，停机问题仅仅只是一个开始。莱斯法则（Rice’s Theorem）证明我们不可能计算任何具备语言特性的程序。迄今为止，任何希望可计算性能够有助于程序的创建或者分析的人一定正陷入绝望之中。这些定理的确证明了通过计算来决定任何程序的适用的语言特性是徒劳无益的，这只是一个对这些结果的天真的曲解。

    每一个编程人员都是通过经验知道无限循环的。有时即使是最好的程序员也会写出陷入死循环的程序，发现循环通常并不是什么大不了的事情――当然这要求你具备相当的经验。实际上，我们解决了自己所写的每一个程序的停机问题。

    等等，你不是说，我们不是计算机所以得不到结果吗。但是如果我们使用某种方式发现或者阻止了循环，那么也就在计算这个答案了。可行的方法就是在更新循环计数器时进行检查。

    怎么会这样？我们并不指望能够计算停机问题，但是实际上我们又时刻在解决它。这是为什么？有规则地计算另外一个特性能够带来一些启发。

    程序中广泛应用的一个语言特性是类型安全，一个由自动类型检查所决定的特性。一个类型安全程序永远不会遇到运行时间类型的错误，例如用一个字符串乘以一个库记录产生的无用信息。

    什么是类型检查？一种测定类型的编程语言需要每一个变量和函数都限制于特定的类型。例如，如果我在程序中使用变量x，那么x的每一次出现都必定是一个数：不必要是同一个值，只需要是同一个类型。VHDL和其它类型的编程人员非常熟悉类型规则，他们知道，直到所有麻烦的类型错误都已经被发现和清除，编译器才会开始翻译代码。由于用类型检查语言写成的程序以后不会产生任何运行时间类型错误，所以等于类型检查清除了一类错误。

    用户在使用诸如Verilog和Lisp等不进行类型检查的语言时，他们明白无论在何时需要使用变量都非常方便。如果他们不得不调试足够的代码，他们将会寻找以意外的方式解释的变量，因为微小的错误可能源于那些无意识的使用。类型错误常常比无限循环更难调试。

    但是言归正传，既然不可能解决停机问题和莱斯法则，为什么可能进行类型检查呢？这个疑团有一个惊人的答案。

    就类