Cella 是什麼？

Cella 是形式化驗證與證明的程式語言。核心是 Cubical 型別論（CCHM）；同一套語法裡還有用量（QTT）、模態（MTT）、定義上的證明無關（SProp）與使用者宣告的改寫規則，由一條定義的 mode 決定它能用哪些（見型別論）。Cella 是證明助理，也能寫、能跑一般的程式。

它給你什麼

• 每一次檢查都有判決：Accept、Reject 或 Unknown，各自說出依據（見判決）。
• 證明：tactic（rfl、intro、induction、simp、ring、omega、linarith、decide…）與 calc。算術的 tactic 在 Rust 裡 找憑證，由 Cella 以計算驗證；求解器是找的人，不是判官。
• 程式：IO、字串、任意精度的 Nat，三個後端：WasmGC（預設）、bytecode VM、NbE 直譯器。型別檢查與執行是同一份語意的兩個投影。
• 洞：程式裡寫 ?name，判決是 Unknown，Cella 列出每個洞的型別、脈絡，以及放得進去的東西。

程式語言，寫成 Cella 的程式

C11、C++17、Arduino 與 ESP32 板子、Python 的語意都以深嵌入寫在 Cella 裡。程式是語法樹；型別檢查把錯誤標在出錯的節點，小步語意負責執行。判決說出它是跑到底、違反了標準的規則（哪一條條文），還是依賴了標準交給實作的選擇。見套件。

用在哪裡

Cella 的第一個應用是 semorphe：用積木和程式碼教程式設計的編輯器，Cella 本身的課程之後也會搬到那裡。第二個是 WebAssembly 的作業系統， Cella 是它的工具鏈與驗證者。