由於這些歸納命題是表現在一階邏輯集合之中的，而後者是不可判定的，我們在正確性證明中遇到了下列的困難。僅當一個程序是正確的時候，正確性證明算法才是有效的；而當這個程序中有錯誤時，這種證明算法將是無結果的。我們將無從知道，這究竟是證明這個程序有錯誤還是說明這個算法不夠強，因而不能證明其正確。目前有兩種繞過這一困難的方法。一種是提出的“程序的邏輯分析法”，另一種是提出的邊寫程序證明的方法。
我們的方法符合並且給的一種洞察提供了形式的實現，他的看法是，我們不應該去從事程序正確性證明，而應該在編一個程序的過程中使它的正確性成為顯然的。接著說：“在我們的方法中，能夠用正確的斤似來生成新的正確的就像能夠將已有的正確的代數或邏輯的公式合並起來生成新的正確的公式那樣。這就提出了下列的對程序設計過程的看法，即程序設計可以看作大致與代數計算類似的一類形式運算，在這種運算中，程序的表示初等的不可歸約的正確的算法片段被組合起來產生出適合這種或那種應用的正確的程序，從這一觀點出發我們可以說，正如同可靠的正確的長的代數公式的產生必須借助於一個公式運算程序，大型的正確的時必須借助於一個程序控製的處理係統的形式的使用。在這兩種情形中，如果我們采用手算，誤差的概率都將要大得不可收拾。
可以應用我們的修改和組合規則的最初等的片段是一些通常相當小的正確的朽。其中的每一個都表示算法的某種基本的和不可分解的元素，為廣論證這一根源？服的正確性，我們得不用於程序驗證技術的一個變種。另一方麵，作我們的方法中，仙的正確性將可以以一種例行的方式從它們的構成方式推出。所以我們可以從應用方時對通常那樣用。方法提出的第二種批評意見是，這種方法對組時成的程序所應用的處理方法實際不是隻需要程序，這樣就使得形式的驗證費時費力。
高階軟件；是最近幾年新發展的技術，隻在個方用過這種技術和通常的測試技術以及結構程序設計聯合起來使用時，是比較是效的。這一技術的要點是用一種軟件：這種語言不同於通常所說的高級語斤）來表達根據這組規則編寫出來的軟件將能夠避免一些常見的邏輯錯誤。高階軟件就是遵守一組基本的形式規則，用一種軟件的元語。
這一組形式規則這一技術也可以稱之為軟件中的一種公理化方法。我們可以將這一技術與集合論中的公理化方法作類比。如所周知.集合論的發展在本世紀初遇到很大的困難，即發現論在這以不久產生了公理化的集合論。在這種公理化集合論中，已知的“悖論”是保證不會有的。因此，集合論中的公理方法實際是一種排除公理係統中某些類鍛的邏輯錯誤的方法。高階軟件技術中的公理方法則是用來排除軟件中某些類型的邏輯錯誤的，並目.所排除的邏輯錯誤中布的是“悖論”十分類似的。
另外，提高軟件可靠性的其他技術，如結構程序設計和程序正確性證明，也是與邏輯中避免“悼論”的其他方案類似的。在邏輯中是由於排中律的濫用，主張在無窮集合的領域排中律。用結構程序設計的人認為，軟件的錯誤叢生，部分原因是由於轉向語句的濫用，主張不用或少用轉向語句。這一相似之處在文獻中已有人指出過。
還有，程序正確性證明在數理邏輯中也有與之相對應的東西，那就是公理係統的協調性證明。