Jsem velmi šťastný z pokroku na HVM4. SupGen je nyní integrován a (konečně) máme integrovaný typový systém, což znamená, že HVM bude fungovat jako super rychlý paralelní ověřovač důkazů. Nepřekvapilo by mě, kdyby to nakonec bylo OOM rychlejší než Lean, a myslím, že by to mohlo být užitečné při konstrukci prostředí RL dokazujících věty. Také: Zase jsem se zamiloval do C. Všechno je teď C, dokonce i parser. Když kódová základna roste příliš rychle, strávím několik dalších výzev jen vyleštěním a vylepšením kvality kódu. Tím se udržuje kódová základna pod kontrolou. Pocházím z Haskellu a oceňuji, jak je vše stabilní a rychlé. Možná nejsme tak daleko od časů, kdy se psaní webových aplikací v C stane skutečně životaschopným