这样说，我的第一层意思是，有关一个程序要做什么的精确数学定义必须作为其构造的本原首先给出。如果缺乏这种定义，或者它过于复杂，我们或许会怀疑将来做出的程序能否真正意味着什么东西。我的信念是，一个程序，抽象地说绝不表示任何东西。要说一个程序表示什么，只能是相对于一个在它之前的意图，无论是以这种或者那种形式表示。在这一点上，我并不反对某些人，他们可能感到用"英语"这个词代替"数学"就更舒服一些。我只是怀疑，能不能交给这样的人一件更困难的工作。
我还认为，这种"回归数学"应该表现在一个真正的程序构造过程之中，其中的工作就是要给程序一种定义良好的意义。这里的想法是让程序构造的技术过程伴随着一个证明构造的类似过程，由它来保证所提供的程序与其预期的意义相符。
同时关注一个程序的体系结构及其证明其实是非常有效的。例如，当证明变得非常难搞时，多半程序也会是那样；而构造证明的各种成分（抽象、实例化、分解）也与构造程序中的那些东西非常类似。理想地说，在一个程序的结构与其正确性的证明之间的关系应该非常紧密，以至我们根本无法查清两者中究竟那个是从另一个派生出来的。而后就可以很合理地说，构造一个程序不过就是构造一个证明。
今天，只有很少的程序是按照这种方式描述和构造出来的。那么，这是不是恰好对应着另一个事实，今天那么多的程序极其脆弱呢？
Jean-Raymond Abrial