形式上可證明的程式語言只是個晦澀的數學/計算機科學概念，無法很好地轉化為現實世界。它們在實際代碼中根本無法擴展。 現實是，如果你想建立一個成功的開發者生態系統，你的語言需要更像JavaScript而不是Haskell。隨著大型語言模型（LLMs）的崛起，這一點尤其真實，擁有更多訓練數據的語言將繼續擴大其市場份額。 我這樣說是因為我最喜歡的程式語言是Haskell，並且我從語言設計到編譯器，甚至到底層數學求解器，都是從頭到尾開發這些系統的。它們無法擴展，因為底層數學求解器呈指數級爆炸。