對於 HVM4 的進展我感到非常高興。SupGen 現在已經內建，並且我們（終於）擁有了一個集成的類型系統，這意味著 HVM 將雙重作為一個超快速的並行證明驗證器。我不會感到驚訝，如果它最終比 Lean 快幾個數量級，我認為這在構建定理證明強化學習環境時會很有用。 還有：我又愛上 C 了。現在一切都是 C，甚至解析器也是。當代碼庫增長得太快時，我會花接下來幾個提示來打磨和提高代碼質量。這樣可以保持代碼庫的穩定。來自 Haskell 的我，欣賞一切是多麼穩定和快速。也許我們離用 C 寫網頁應用程序變得實際可行的時代不遠了。