在大企業公司中，合同條款稽核是法務的重要內容，現今的企業大都有合同管理資訊系統，透過資訊系統運轉合同，經過資信調查、文字稽核以及履約監控，基本上可以實現合同風險的管控。其中，文字稽核通常也可以在資訊系統中設定合同範本模板，將格式合同和非格式合同分離，預先設定好合同的條款，防控風險。其它非格式條款就由法務人工稽核，大多數合同管理資訊系統，也是按照上述框架設定。我稱之為“機械式”稽核。
其次，隨著人工智慧的普及化，據聞華爾街已經有軟體可以實現一秒內稽核數千份合同的智慧系統，可稱為“黑盒化”稽核。此類技術只看結果，過程難以解釋，暫不在本文內討論。
再次，合同文字具體內容也並非自然語言般複雜和多義。法律本身就是人類智慧高度理性的結晶，法律語言是在自然語言與社會、倫理、道德等諸多領域交匯協調後的高度抽象產物。我以為：可以把法律語言和C++、Rust 、Lisp等語言一起並列，也是一種程式語言，可稱之為Law語言，簡稱L語言，只是它實現的目標和展現的方式更加宏大而已，學習曲線更加陡峭吧。
L語言既然是一種程式語言，而合同是純粹的法律語言構成，那麼，自然可以在合同文字中找到程式語言的諸多共性，同時，合同文字也必須是一種靜態語言（因為用動態語言充滿了歧義，不適用於L語言），既然是靜態語言，那麼合同文字必須要遵循型別約束，同理，反之，可以從型別約束來格式化規範合同文字，如果型別出錯，那麼合同文字或條款的設定就有問題，透過型別約束來編譯合同，既可以實現計算機協助稽核的目標，又可以清晰地解釋稽核過程和出錯原因，我稱之為“半自動化”式合同稽核，這也是本文討論的重點。
如今，隨著React、Vuejs、Flutter、SwiftUI等框架的發展，越來越多的程式設計者朝著型別不變性和函式式邁進。他們使用HTML和CSS之類的“DOM模型”進行程式設計，其狀態管理不是透過類和物件進行，而是透過類似於Reactor/Redux中的reducers和不可變狀態進行。HTML是函式式的，我以為這是前進的正確方向，但是仍有很多改進的空間。我們看一個例子，在一張紙上畫一個圓和一個方形：
命令性是這樣的：
1、將鉛筆移動到座標（100、100）處；
2、用紅色的鉛筆；
3、畫一個半徑為20的圓；
4、概述您的草圖；
5、將鉛筆移動到座標（200、100）處；
6、用藍色鉛筆。
7、繪製一個寬度為50，高度為30的矩形。
8、在瀏覽器上渲染出來。
上述是前端程式設計的一個簡單命令式描述。可以看到，動作是一步步走的，而且要用不少言語，當然它的好處就是簡單明瞭。再看看函數語言程式設計，相對於命令式，函式式更像是對圖紙上畫的物體的高階解釋：
1、圖片由兩個彼此重疊的物件組成：
2、在（200、100）處，是一個藍色的矩形，寬度為50，高度為30；
3、在 （100、100）處，半徑為20的紅色輪轂圓圈。
同樣的工作，命令式用了8句，函式式只用了3句。高階解釋就是函式式的優點，它的第二個優點就是型別約束。函式式語言與靜態型別是相生相成的，因此，靜態型別能提高函式式的執行速度，以及規範解釋性。例如：
1、畫圖：座標數字 -> 字串
2、畫圖 座標數字 =
將座標數字轉成字串的函式 座標數字
第一行規定的就是該函式的靜態型別，意即輸入引數為數字，輸出結果為字串，所以如果把一串字元作為引數餵給畫圖函式，編譯器就會出錯，而且清晰地給出出錯原因。拓寬思維去想一下，把畫圖函式轉成合同某條款的文字函式：
1、違約金條款 ： 本金->比例->時間->金額 （靜態型別）
2、違約條款 本金 比例 時間 = （函式）
本金X比例X時間
上述例子中，違約金條款受靜態型別的約束，規定是遵循“本金、比例、時間”的循序輸入，違約條款的函式描述也非常清晰，輸入引數三者相乘得出本金。在這裡，特意選擇了違約金條款進行函式化和型別靜態化，因為違約金條款都是數字，和一般程式語言的數學演算法處理一致。但是要注意的是 違約條款函式 已經超出了一般程式語言的涵義，它也代表了合同文字描述的格式化和規範化，如果企業合同文字違化了這種格式，就會編譯出錯和提示原因。
這種函式式的稽核方式，是透過把合同文字編寫規範轉成函式，透過型別簽名的輸入引數型別、輸入順序、輸出結果型別以及函式內容來描述合同文字規範和規律。下一節，我們再嘗試把更復雜的合同文字轉化成帶有靜態型別的函式。
