所說的“程序自動綜合”有兩種.一種是通過程序工具的改進提高自動化程度（可以稱之為“通過工程方法”的），另一種則是借助於構造性證明的機械化（可以稱之為“通過構造性數學方法”的），以下我們分別討論這兩種程序綜合。
通過工程方法的程序綜合
這種程序綜合係統是現在已經實現了的。美國康奈爾大學五年前設計出來的“康奈爾程序綜合係統”即是一例。這種係統是借助於編譯程序、排錯程序和編譯程序等等來進行綜合的。隨著這些程序工具效率的提高，程序設計自動化的程度將不斷提高，這就是人所預測的未來程序設計的發展方向。
通過構造性數學方法的程序綜合
這是利用數學定理證明（具體說來是構造性數學的證明）和程序設計的相似性，通過證明來編製程序的方法。在1947年寫成的一篇論文中就提出過這種思想論文載在1969年出版的《第四屆機器智能討論會論文集》中，但沒有引起注意。六十年代末和七十年代初美國的獨立地提出了這種思想。
這種思想可簡要地說明如下，設有可計算函數，而要求寫出一個求？的值的程序，並設已知，我們可以先設法證明，並使這一證明為構造性的（即不使用反證法這一證明中將隱含求的值的算法。於是可以從這一證明中提取出算法從而得出程序。
這在概念上是簡單而直捷的，是巧妙的，問題在於效率。美國斯坦福大學的多年來合作，從程序自動綜合的研究。他在1985年12月來北京訪問，在一次講演後回答問題時說，他們的方法目前還隻能用於很短的程序（例如解後問題的程序），要過時間以後才可以用於現實的程序。這一方法的創始人之一，1986年7月和我一起參加召開的“計算機科學與數理邏輯國際合作會議”。在會議期間和我的私人談話中，他對我說“對於通過數學定理的機械化證明來實現程序自動綜合的前景我是持懷疑態度的。他解釋說，他是最早提出定理證明和程序設計的相似性的人之一。他指出構造性數學證明中隱含有算法，但現在他對於通過定理的機械化證明來實現程序的自動綜合表示懷疑。
對於通過數學方法來實現程序綜合這一方向另一種懷疑意見是認為，為了推廣這一方法需要對成千上萬的普遍程序設計人員進行數理邏輯的再訓練，而不少計算機科學家認為這是不大可行的。
還有-些計算機科學家認為，就形式方法在軟件技術方麵的應用而言，通過構造性數學的方法來實現程序綜合可能是目前離實際應用最遠的一個方向。
程序再用技術的自動化
數理邏輯曆史上曾有人提出，可以比照函數演算（即2演算）而建立一種程序組合演算。看來這種組合演算是會對我們在此處提出的“自動的程序再用技術”有用的。
現代數理邏輯的兩個問題及其哲學涵義
現代數理邏輯包括下列一個分支證明論，②模塑論，③可計算性理論，④公理化集合論，⑶計算機科學的數學基礎。本文從④和⑤中各選出-一個著名的未解決的問題。
現代數理邏輯中有兩個著名的未解決的問題，即連續統問題（或者說實數有多少的問題或者說機械算法與非機械算法所能解決的問題是否一樣多的問題）。這兩個問題分別是集合論與計算機科學的數學基礎中帶根本性的問題。前一個問題在數學中具有重大意義，是集合論的奠基人在距今一百年前提出來的，至今我們不知道它的答案；而且已經知道，在通常的集合論中這個問題不可能得到解決的。後一個問題是70年代初提出來的，具有重大的理論意義和實際意義。現在已經知道，這個問題得到解決，將有幾百個數學問題（其中包括一些有重要實際意義的問題）都連帶得到解決。但這個問題和前一個問題一樣是難度很大的。最近有人猜測，這個問題在通常的公理化算術中是無法解決的。可能和前一個問題一樣在通常的集合論中也是不可能解決的。正是由於這兩個問題的關鍵性，目前有許多人在進行研究。還有一些人的工作表麵上看來和這兩個問題沒有聯係，實際上也是為了以後去攻其中的一個做準備。