Дуже задоволений прогресом на HVM4. SupGen тепер вбудований, і ми нарешті маємо систему рідного типу, що працює безпосередньо в мережах взаємодії, що означає, що HVM можна буде використовувати як швидкий, паралельний верифікатор доказів. Я не здивуюся, якщо він виявиться швидшим, ніж Lean, і я хотів би застосувати це до доведення теореми RL Крім того, кодування штучного інтелекту робить C напрочуд життєздатним. Кодова база HVM тепер на 100% складається з C - парсер, оцінювач, шашка, все - і я все ще повністю контролюю її. Коли він зростає занадто сильно, я витрачаю наступні кілька підказок, щоб просто відшліфувати та покращити якість коду. Це дуже важливо, щоб тримати його під контролем. Працюючи в Haskell, я ціную, наскільки стабільно і швидко все працює в C (і нарешті я можу використовувати 100% свого процесора за один раз!)