語言可能至今仍是他個人的語言，美國有些計算機科學家認為這是一種供理論研究用的理想語言，何至今隻有少數人重視它。
變換型程序設計
變換程序設計、程序驗證和程序綜合三者都屬於“程序設計方法學”的範圍。我們將在本節和以下兩節中分別加以介紹，特別說明它們和邏輯的關係。
變換型程序設計將程序生成的過程分為兩個階段，即給出用戶需求的形式說明，由用戶需求的形式說明出發，應用給定的形式變換規則，迸行-係列的變換，最後得出可以在機器上執行的程序。這種設計方法最早可能是英國人提出來的。近年來最為人注意的可能是西德慕尼黑科技大學研製出來的係統。這一係統已研製了十年，聽說他們正在和有的軟件公司商談，希望將他們的這一結果變成軟件產品。
就是依照上述思路設計出來的。在這種設計中，構造形式說明和進行變換這兩個階段中都大量地應用了形式方法即邏輯方法。所用到的變換規則是由邏輯中的推理規則演化而來的。這種設計方法是否有實際意義決定於所用的變換規則的效率。而言，有人懷疑其中的變換規則在機器上實現時效率仍嫌過低。因之它能否在最近幾年內就成為軟件產品是頗成疑問的。
程序驗證
程序的可靠性一直是程序的關鍵問題，因為不可靠的程序就是質量不合格的程序，有時要誤大事人們使用計算機以來幾十年的經驗是：要做到使程序不出錯誤是很困難的，要使得大程序(即幾萬行以至幾十萬行的程序）不出錯誤，就更是難上加難了。
從60年代中期到70年代中期這十年中，曾有一些人從事程序正確性證明的研究。所說的程序正確性證明就是在一個特定的程序寫成以後，用數學方法來證明這個程序的輸人和輸出關係(可以看作是一個函數）正好是原來的用戶需求所要求的那樣。具體方法是證明一對特定的輸入謂詞和輸出謂詞之間存在著推導關係。
這種證明方法到70年代中期已經發現，隻能用於很短的程序，而不適用於實際的程序。在此以後，不少計算機科學家指出，用形式方法驗證程序其他的途徑。途徑之一是美國人提出的“正確程序技術”
這種途徑的基本思想大致如下：先建立一個基本程序庫。這種基本程序都是一些可以用來構成大程序的簡短程序，然後再找出一組程序組合規則，借助於這一組規則可以從簡短的基本程序構造出多種多樣的複雜的大程序。隻要我們能保證基本程序中的程序都是能保持正確性的，則這樣組合出來的程序將可以保證都是正確的。
已提出一組程序組合規則，並已證明這些規則是能夠保持正確性的。但要建立一個所需要的基本程序庫卻是--項浩繁的工作。1977年時曾估計約需要十年的時間，目前這一項目的進展如何，則不清楚。
程序綜合
這裏所說的“程序綜合”是指“程序的自動生成”（嚴格說來是“部分的自動生成”）。所說的“程序的自動生成”或“自動程序設計”又有廣義與狹義之分，而且是在不同的時期有不同的意義。50年代所說的“程序沒動化”即指編表也就是由機器將用高級語言寫出的程序變換成某種類型的計算機程序。就這點而現作已完個能做到。我們這裏說的“程序自動生成技術”。
因此比較實用的方法。一般的看法認為通過程序工具與環境的研究，程序開發的自動化程度將不斷提高。預計在本世紀90年代可望有明顯的提高。到了下一個世紀的前半，程序開發將可以高度自動化。