在這裏，準備隻介紹數理邏輯在軟件方麵應用的兩三個例子。
我們在下麵先簡單介紹一種程序設計語言，然後講兩個題目，即程序設計語言語言方麵的形式定義；邏輯在軟件可靠性技術方麵的應用。這裏隻舉了兩個邏輯在程序方麵應用的例子，還有一些同樣重要的應用沒有提到，如形式方法的研究是有重要應用的，而我們今天就不準備介紹了。
一種程序設計語言
電子計算機之所以能夠以高速度自動完成一係列的運算，是因為有人事先編好了程序，存在機器中。這種程序是由機器指令構成的。編這種程序是一件費事。後來產生了這一種類似數學記法的語言。這種語言人們稱之為程序設計語言又叫算法語言或高級語言用這種語言編出來的程序比用機器指令編的要簡短得多。我們可以用這種語言編寫程序，然後由機器將這樣的程序翻譯成用機器指令構成的程序，再存機器上執行。下麵是一個用程序設計語言的程序的例子。留出位置；同時說明這些數量都是整數。這種語句稱作“說明”。第二行告訴計算機，從紙帶入四個數，將這些數送入為等保留的存貯位置。
程序設計語言語言方麵的形式定義
數理邏輯的許多種算法理論可以用來為程序設計語言提供語言的形式定義，而語言的形式定義在實際工作中是有用的。第一，它對設計語言有用，可以用來檢查一種語言是否有不—致之處。還有，有些語言的設計是受了形式定義的啟發的，對形式定義的研究對語言的設計有啟發。第二，對寫編譯程序有用，因為這種形式定義對於要為之編寫編譯程序的語言，提供了嚴格定義。在這方麵，目前可供使用的理論工具不止一種。廣義計算法雖然未必是目前最好的理論工具，但它在直觀比較清楚，容易說明。這方麵的情形請參看《計算機硬件與軟件設》。
邏輯在技術方麵的應用
第一代計算機的軟件結構複雜，如何排除邏輯錯誤成了大問題出來，問題不大，問題在於如何排除邏輯錯誤，近年來在這方麵遇到了很大困難。西方國家的軟件工作者所說的軟件危機的主要表現之一就是大的軟件可靠性差，錯誤百出。60年代有的發達國家在多方麵失敗。該國的一些大的計算機的操作係統在經過長時間的調試而交付使用，還包含著大量的錯誤。發現了大量的錯誤。
工作者在不斷地探索提高軟件可靠性的新途徑、新技術。已經在試用的有結構程序設計、程序正確性證明和高階軟件（這是一種應用公理方法的技術）等。數理邏輯在這三種新技術中都可以.有應用，特別是後兩種技術要用到邏輯。我們在下麵簡單介紹邏輯在這兩種技術中的應用。
程序正確性證明
通過嚴格證明來驗證程序正確性的思想，在電子計算機產生後不久就有人提出來過。1950年時就曾有人證明方法來驗證了一個程序的正確性。但後來長時間沒有人從事這方麵的工作。1966年才又有人提出了證明程序正確性的方法。但這一技術目前隻能用於較短的程序。用這種方法證明過的最長的程序是一個行的編譯程序是一個子集的編譯程序要達巍能比較廣泛實際應用的思度迄今仍有不小的距離。
程序正確性證明有非形式的與形式的兩種。前者的主要方法叫做“歸納命題法”。這個方法的主要思想是，在一個程序和它的輸入謂詞與輸出謂詞給定後，通過證明一組關於這個程序中的若幹重要變量的命題之間存在著蘊涵關係，來證明這一程序的正確性。我們現在通過一個簡單的例子來說明這一方法。是一個除法程序，用以實現正整。閃為每經過一次循環這個程序是正確。