Sehr glücklich über die Fortschritte bei HVM4. SupGen ist jetzt integriert, und wir haben endlich ein natives Typsystem, das direkt auf Interaktionsnetzen läuft, was bedeutet, dass HVM als schneller, paralleler Beweisverifier nutzbar sein wird. Es würde mich nicht überraschen, wenn es am Ende OOMs schneller als Lean ist, und ich möchte es auf das Theorembeweisen RL anwenden. Außerdem macht das AI-Coding C überraschend tragfähig. HVMs Codebasis ist jetzt zu 100 % C - Parser, Evaluator, Checker, alles - und ich habe immer noch die volle Kontrolle darüber. Wenn es zu groß wird, verbringe ich die nächsten mehreren Eingaben nur damit, den Code zu polieren und die Codequalität zu verbessern. Das ist sehr wichtig, um es im Zaum zu halten. Aus der Haskell-Welt kommend, schätze ich, wie stabil und schnell alles in C ist (und endlich 100 % meiner CPU nutzen zu können!)