Bardzo się cieszę z postępów w HVM4. SupGen jest teraz wbudowany, a w końcu mamy natywny system typów, działający bezpośrednio na sieciach interakcji, co oznacza, że HVM będzie użyteczny jako szybki, równoległy weryfikator dowodów. Nie zdziwiłbym się, gdyby okazał się OOMs szybszy niż Lean, a chciałbym zastosować go w dowodzeniu twierdzeń RL Ponadto, kodowanie AI sprawia, że C jest zaskakująco wykonalne. Kod źródłowy HVM jest teraz w 100% w C - parser, evaluator, checker, wszystko - i wciąż mam pełną kontrolę nad tym. Kiedy staje się zbyt duży, spędzam następne kilka podpowiedzi, aby dopracować i poprawić jakość kodu. To bardzo ważne, aby to kontrolować. Przechodząc z Haskella, doceniam, jak stabilne i szybkie jest wszystko w C (i w końcu mogę wykorzystać 100% mojego CPU po raz pierwszy!)