「Program=Proof筆記」修訂間的差異

於 2023年6月25日 (日) 17:28 的修訂

題名：Program=Proof

中譯：證明=程式

作者：Samuel Mimram

---

開頭作者舉例一個式子在數字很大的時候會出錯的案例，來說明證明的重要性。

之後提到證明即程式（利用程式的性型別）的概念。

檢查程式：

空中巴士公司使用形式方法來驗證程式是否出錯誤。

CompCert 用 coq 來造出證明程式符合語義的C編譯器。

自動化證明：

證明數學是一種藝術。和驗證是否錯誤比，較難。就如積分比微分難一樣。

依值型別：

(* 註解*)

@@ 行 5： / 行 5： @@
 ---
+==== Ch0 序言 ====
 開頭作者舉例一個式子在數字很大的時候會出錯的案例，來說明證明的重要性。
@@ 行 24： / 行 25： @@
 * Agda 與 Coq 幫助漸次展開證明
 * 證明時間 > 測試時間
-* 重要的軟體被證明
+* 重要的軟體使用之驗證
+==== Ch1 Ocaml ====
+(* 註解*)
@@ 行 31： / 行 34： @@
-[[categoty:資訊]]
-[[categoty:邏輯學]]
+[[:分類:資訊|category:資訊]]
+[[:分類:邏輯學|categoty:邏輯學]]