HVM4の進歩に非常に満足しています。SupGen が組み込まれ、ついにインタラクション ネット上で直接実行されるネイティブ型システムが完成し、HVM が高速で並列証明の検証ツールとして使用できるようになります。Leanよりも速いOOMになっても驚かないでしょうし、RLを証明する定理に適用したいと思います また、AI コーディングにより、C は驚くほど実行可能になっています。HVMのコードベースは100%C(パーサー、エバリュエーター、チェッカーなど)であり、私はまだそれを完全に制御しています。大きくなりすぎると、コードの品質を磨き、改善するためだけに、次のいくつかのプロンプトを費やします。それを抑制することは非常に重要です。Haskellから来て、私はCですべてがどれほど安定していて高速であるかに感謝しています(そしてついにCPUを100%使用できるようになりました!