形式的に証明可能なプログラミング言語は、現実世界にうまく変換できない難解な数学/CS のアイデアにすぎません。実用的なコードには拡張できません。 現実には、開発者エコシステムを成功させたいのであれば、言語は Haskell よりも JavaScript に似ている必要があります。これは特にLLMの台頭に当てはまり、より多くのトレーニングデータを持つ言語が市場シェアを拡大し続けるでしょう。 私は、Haskell がお気に入りのプログラミング言語であり、言語設計からコンパイラ、さらには基礎となる数学ソルバーに至るまで、これらのシステムをエンドツーエンドで開発してきた者としてこれを言います。基礎となる数学ソルバーが指数関数的に爆発するため、スケーリングされません。