Rất vui về tiến trình của HVM4. SupGen giờ đã được tích hợp, và cuối cùng chúng ta có một hệ thống kiểu dữ liệu bản địa, chạy trực tiếp trên các mạng tương tác, có nghĩa là HVM sẽ có thể được sử dụng như một trình xác minh chứng minh nhanh và song song. Tôi sẽ không ngạc nhiên nếu nó nhanh hơn OOMs so với Lean, và tôi muốn áp dụng nó vào việc chứng minh định lý RL Ngoài ra, lập trình AI đang làm cho C trở nên khả thi một cách bất ngờ. Mã nguồn của HVM giờ đã 100% là C - trình phân tích, trình đánh giá, trình kiểm tra, mọi thứ - và tôi vẫn hoàn toàn kiểm soát nó. Khi nó phát triển quá nhiều, tôi dành vài prompt tiếp theo chỉ để làm sạch và cải thiện chất lượng mã. Điều đó rất quan trọng để giữ nó trong tầm kiểm soát. Xuất phát từ Haskell, tôi đánh giá cao sự ổn định và nhanh chóng của mọi thứ trong C (và cuối cùng có thể sử dụng 100% CPU của tôi một lần!)