Veldig fornøyd med fremdriften på HVM4. SupGen er nå innebygd, og vi har (endelig) et integrert typesystem, noe som betyr at HVM vil fungere som en superrask, parallell bevisverifikator. Jeg ville ikke bli overrasket om det ender opp med å bli OOM-er raskere enn Lean, og jeg tror det kan være nyttig når du konstruerer teorem som beviser RL-miljøer. Dessuten: Jeg er forelsket i C igjen. Alt er C nå, til og med parseren. Når kodebasen vokser for fort, bruker jeg de neste spørsmålene bare på å polere og forbedre kodekvaliteten. Dette holder kodebasen i sjakk. Når jeg kommer fra Haskell, setter jeg pris på hvor stabilt og raskt alt er. Kanskje vi ikke er så langt unna tider når det å skrive nettapper i C faktisk blir levedyktig