Bardzo się cieszę z postępów w HVM4. SupGen jest teraz wbudowany, a my (w końcu) mamy zintegrowany system typów, co oznacza, że HVM będzie działać jako super szybki, równoległy weryfikator dowodów. Nie zdziwiłbym się, gdyby okazało się, że jest OOMs szybszy niż Lean, a myślę, że to może być przydatne przy konstruowaniu środowisk RL do dowodzenia twierdzeń. Również: znów zakochałem się w C. Wszystko jest teraz C, nawet parser. Kiedy baza kodu rośnie zbyt szybko, spędzam następne kilka promptów, aby dopracować i poprawić jakość kodu. To utrzymuje bazę kodu w ryzach. Przechodząc z Haskella, doceniam, jak stabilne i szybkie jest wszystko. Może nie jesteśmy tak daleko od czasów, kiedy pisanie aplikacji webowych w C stanie się naprawdę wykonalne.