HVM4の進歩に非常に満足しています。SupGen が組み込まれ、(ついに) 統合型システムが完成したため、HVM は超高速の並列証明検証ツールとしても機能します。Leanよりも高速なOOMになっても驚かないでしょうし、定理証明RL環境を構築するときに役立つと思います。 また、私は再びCに恋をしています。パーサーも含めて、すべてがCになりました。コードベースの成長が速すぎると、次のいくつかのプロンプトをコードの品質を磨き、向上させるためだけに費やします。これにより、コードベースがチェックされます。Haskell から来た私は、すべてがいかに安定していて速いかを高く評価しています。おそらく、C で Web アプリを書くことが実際に実行可能になる時代からそれほど遠くないでしょう