Molto felice dei progressi su HVM4. SupGen è ora integrato e finalmente abbiamo un sistema di tipi nativo, che funziona direttamente su reti di interazione, il che significa che HVM sarà utilizzabile come un verificatore di prove veloce e parallelo. Non sarei sorpreso se risultasse essere OOMs più veloce di Lean, e mi piacerebbe applicarlo alla dimostrazione di teoremi RL Inoltre, la programmazione AI sta rendendo il C sorprendentemente praticabile. Il codice di HVM è ora 100% C - parser, valutatore, controllore, tutto - e ho ancora il pieno controllo su di esso. Quando cresce troppo, passo i successivi diversi prompt solo per lucidare e migliorare la qualità del codice. È molto importante tenerlo sotto controllo. Venendo da Haskell, apprezzo quanto sia stabile e veloce tutto in C (e finalmente poter utilizzare il 100% della mia CPU per una volta!)