Cella Lang

第一次來？ Cella 是一種讓電腦逐步核對的語言：可以在裡面寫數學證明，也可以把一支 C++ 或 Python 程式放進來檢查。 每次核對的結果只有三種：對；錯，並指出錯在哪裡；還無法確定，並說明卡在哪裡。它確定不了的時候會直說，不會猜一個答案給你。

用過 Lean、Coq 或 Agda？ Cella 是同一類的證明語言，以立方型別論（CCHM）為核心，型別檢查通過的定義就是成立的證明。 不同的地方：每次檢查以 Accept、Reject、Unknown 三種判決之一結束，並列出它依賴的假設；C、C++、Arduino、Python 以深嵌入寫在 Cella 裡，所以「這支 C++ 程式沒有未定義行為」是可以證明的定理；整個檢查器編成 WebAssembly，在瀏覽器裡就能跑。

試試看

三個範例，給不同的人：分頁切換後會自動執行，判決與輸出顯示在右邊；程式可以直接改，再按「檢查」或「執行」。完整的編輯器與更多範例在編輯器。

判決，不是布林

檢查器說「通過」的時候，你應該知道它驗了什麼。Cella 的每一次檢查，都以三種判決之一結束。

Accept（接受）

兩個獨立的 kernel 都驗過，並列出它依賴的假設：某個 postulate、某條改寫規則、由 elaborator 判斷的終止性。

Reject（拒絕）

有錯，並指出在哪裡、違反哪一條規則。

Unknown（未知）

還不知道，並說出原因：有洞、步數預算用完、依賴的定義本身是未知。Unknown 會傳染：依賴它的也不是 Accept。

兩個獨立的 kernel：一個錯騙不過兩個

elaborator 用的 kernel 求快。另一個檢查器從零獨立寫成、不和前者共用程式碼，照型別規則逐條實作，重驗每一條定義；兩邊不一致就大聲失敗。每一條型別規則都有必須接受與必須拒絕的語料。

同一套語法、多種型別論，由 mode 選擇

Cubical 型別論

CCHM：路徑、transport、Glue、高階歸納型別。univalence 會計算。

用量與模態

QTT 的 grade（抹除、線性、不限）與多模態型別論，兩個 kernel 都檢查。

證明無關與改寫規則

定義上的證明無關（SProp），不推出 K；使用者宣告的改寫規則，檢查每個臨界對。

mode

每條定義宣告它在哪個 mode，只為用到的特性付代價；「這個證明沒用到 univalence」是可以檢查的事。

程式語言，寫在 Cella 裡

C11、C++17、Arduino 與 ESP32 板子上的 C++、Python 都是深嵌入：程式是一個值，型別檢查與小步語意寫在 Cella 裡，所以一支 C++ 程式有沒有未定義行為，是可以證明的命題。這些模型和真的工具做差分：clang 加上它的 sanitizer、avr-gcc 與 simavr 模擬器、CPython。模型能報的每一種未定義行為，都有一對在這些工具上量過的最小程式，釘住它的邊界。

在瀏覽器裡跑

檢查器編成 WebAssembly；程式編成 WasmGC，在瀏覽器、Node 與 ESP32 上原生執行。在 JavaScript 裡經由 npm 套件 cella-lang 與 @cella-lang/* 使用。