一、導言
這裏所說的邏輯包括證明論，模型論，遞歸論和公理集合論。近年來，人們愈來愈認識到邏輯對程序設計是有用的。這兩門科學之間的密切關係可以用？提出這種關係從另一角度來加以說明，即可以將推理看作非確定性算法。
在50年代後期，蘇聯數學家曾指出，“遞歸函數論”可以用作表示-台計算機或一個程序的理論。他們指出，一台計算機可以看作--組寄存器，這寄存器在時間，所以在1960年指出了同一事實，他在他所寫的《構造性分析基礎》一書中說，“遞歸函數論”可以看作一種程序設計語言（即一種非過程語言）。
在60年代初，建立計算機語言，這種語言是以建立的定義在符號表達式上的“遞歸函數論”為基礎的。其他幾位邏輯學者（包括中國的胡世華先生）差不多同時發展了這種理論。60年代中期，開始了利用歸納斷言法進行程序正確性證明的研究，則開始了利用構造性證明進行程序綜合的研究。這兩個方向都用了數理邏輯的方法。也許可以指出，在40年代後期已經指出了這兩個方向。後者包含在他在1947年寫成的備忘錄中（發表在1969年出版的《機器智能第四屆討論會論文集》中他的關於程序正確性證明的論文發表在1951年出版的《劍橋大學數學雜誌》上。顯然這兩種想法都不為計算技術界所知，重新提出。
1969年出現了一階邏輯的兩種拓廣的形式，這兩種邏輯都能夠更有效地表示有關程序的推理。其中一種是和華沙大學的如七等人提出的算法邏輯，另一種是提出的程序設計邏輯。值得指出，前者是建立在更廣的基礎上，也就是建立在之上（這是一種“無窮邏輯”，其中包含有可數無窮長合取式），後者則是建立在通常的邏輯基礎的不同，―者的表達能力是不同的。已經證明，前者是完全的，而後者是不完全的（所說的完全性是說，一切正確的程序都是能夠在這種邏輯中證明為正確的）。
在70年代初，考瓦爾斯基和柯爾摩等人提出了用“一階邏輯”作程序設計語言的思想。柯爾摩在別人的協助下設計出來了的語言，這種語言現在已廣泛為人所知。這種語言近年來引起很大興趣，因為它可能適合用智能機，就像日本新一代計算機的設計者們所想的那種機器，程序設計語言的形式語言學已被公認為理論。對於“一個程序的語言是什麼？”這個問題是的答案的。現在至少有三種不同的研究角度。
此外，在多項式時間內完成的非確定性算法過程可能是一種並行過程。但我們在這方麵的知識是非常有限的。
邏輯程序設計
一般認為，用一階邏輯作為新一代計算機的程序語言的想法在理論上是可行的，但柯爾摩等人原提出的語言即？計算機語言卻是有缺點的。一方麵語言沒有利用“一階邏輯”的全部表示能力，另一方麵這種語言中有些特點在“一階邏輯”中是沒有與之相應的東西的。
發展了一種新的計算機語言，這種語言將？這種語言與泛函程序設計語言相結合，使得可以使用邏輯變量，於是這種語言將能夠對用戶定義的抽象數據類等式進行求解。
一般認為漢語言的邏輯基礎，所說的其他特點如多種類變量就是一例，這一特點由於其對類型的影響是有用的。
邏輯與程序設計方法學
如前所述，在計算技術方麵進行了開創性工作的少數數學家和邏輯學家已經對程序設計的數學基礎問題感興趣，例如在40年代後期已對這類問題感興趣。曾說，可以證明數學定理那樣來證明一種計算機設計的正確性。指出，定理證明與計算機程序設計之間的令人感興趣的關係在於下列的事實，即可計算函數程序可以在有關的數學命題構造性證明中提取出來。構造性數學的這一出人意料的在程序設計中的應用一直未受人注意，直到60年代末重新發現了這種可能性。從那時起已進行了大量,但必須指出，目前程序綜合的工作大部分是利用經驗方法完成的，而不是利用形式方法；看來理論工作者和實際工作者要互相配合進行大量的工作，才能使這一方向成為有實際意義的。
邏輯方法應用於程序設計的另一領域是程序正確性證明，這一領域已引起存大學者更人的注意。已出現了大量文獻，提出了各種研究角度，而後來許多研究工作者逐步認識到這一方向是缺乏實際意義，70年代中期曾尖銳地指出，在一個大程序編完之後再試圖進行驗證可以比作將拉車的馬係在車後。這一觀點已為許多人所接受。用正確性的組合規則，從已經過測試或證明的基本程序出發來研製大程序的思想看來是有希望。