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