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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    就类型检查而言，程序可以分为三种：

    1．   能够被类型安全识别的程序。

    2．   明显将要遇到运行时间类型错误的程序。

    3．   我们无法判断是否会遇到运行时间错误的程序。

    第三种程序是有趣的类型。根据程序的输入，此类程序中有些可能遇到类型错误，而许多则永远不会。唯一识别的方法就是运行他们，然后观察是否会发生错误。这就是为什么尽管莱斯法则是正确的，但同时我们仍能够测定类型安全：类型检查能够识别一些表现出这种特性的程序，但并非所有程序都拥有这种特性。一个由类型检查进行校验的程序能够保证是类型安全的，但一个被拒绝的程序并不一定遇到了类型错误。

    每一位Verilog程序员都知道，类型检查有些过于悲观。许多有用且有效的程序永远不会遇到运行错误，却被类型检查拒绝。出于这个原因，许多程序员抛弃了类型检查，因为它实在束缚太多。但是，类型检查语言的程序员知道类型安全的程序太多并且易于构建，因此他们并不介意类型检查将其它有用的程序拒之门外。这是以适当的自由度去换取安全性。

    同样的推断也适用于停机问题：你可以为许多程序解决停机问题――但在那些由于不能确保停机而被拒绝的程序当中，一定有些程序确实会停止。一般来说，没有人会介意：你可以创建足够的经确认要停机的程序，这样就永远不会错过那些可计算性不能识别但是会停机的程序。

    为什么没人构建一个停机推理机制？有些显而易见的原因：

    1.  如上所述，解决停机问题无关紧要。大部分程序员并不为此烦恼。

    2.  大部分编程语言具有复杂的语言特性（对杂乱无章的语言的委婉说法），进行这样的分析即使可能也会非常困难。

    3.  历代计算机科学家已经被告知他们不可能解决停机问题，所以他们为何还要去尝试呢？

    虽然停机问题和类型检查一样可以解决，但是没有人能够提供一个解决方案。不过在半导体设计领域却并非如此。

    由于将一块芯片的RTL价值转化成实际可用的芯片是一个耗时和昂贵的过程，我们想要确保在制作之前RTL至少在逻辑上是正确的。我希望能够奇迹般地清除所有错误――但是这不可能，如果能够保证消除所有能自动检查出的错误，我已经非常满足。有几类错误（例如后稳定性交叉时钟域和输入输出错误）可以通过形式方法和工具来解决。

    为什么出现了用于RTL分析的形式方法，却没有解决停机问题的工具呢？

    比较上述提及的三个原因：

    1.  测试RTL是一件非常重要的事情。在一次性测试环境下，很难以ad hoc的方式证实它是正确的。与停机问题不同，人们乐意付钱来帮助测试已知的问题。

    2.  RTL必须支持确定性的和可预测的综合情况。所以RTL比一般性的编程语言和语法清洁器要更受限制。

    3.  没有人告诉工程师这是不可能的！没有人愿意教授工程师可计算性。由于工程师不知道这是不可能的，所以他们这么做了。现在RTL上正计算着有用的特性。

    这就是为什么我相信形式分析的出现（如EDA工具）代表了一个重大的成就。这些方法形式上是可靠的，并且在实践中证明了它们的价值。形式方法具备改进芯片开发和可靠性的重要且可能难以估量的潜力。

    又有谁能知道，或许计算机科学家某一天一觉醒来，发现同样的事情对于编程语言也是可能的呢。

    (此稿件由PMC-Sierra公司提供)