對於 HVM4 的進展我感到非常高興。SupGen 現在已經內建，並且我們終於有了一個原生的類型系統，直接在互動網絡上運行，這意味著 HVM 將能作為一個快速的並行證明驗證器。我不會感到驚訝，如果它的速度比 Lean 快幾倍，我想將其應用於定理證明的強化學習。 此外，AI 編碼使得 C 語言變得意外可行。HVM 的代碼庫現在是 100% C - 解析器、評估器、檢查器，所有一切 - 而我仍然完全控制它。當它增長過多時，我會花接下來的幾個提示來打磨和提高代碼質量。這對於保持其穩定性非常重要。來自 Haskell 的我，欣賞 C 語言中一切的穩定性和速度（終於能夠充分利用我的 CPU！）