Rất vui về tiến trình của HVM4. SupGen giờ đã được tích hợp, và chúng tôi (cuối cùng) có một hệ thống kiểu tích hợp, có nghĩa là HVM sẽ hoạt động như một trình xác minh chứng minh siêu nhanh, 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 nghĩ điều đó có thể hữu ích khi xây dựng các môi trường chứng minh định lý RL. Ngoài ra: Tôi lại yêu C. Mọi thứ giờ đều là C, ngay cả trình phân tích cú pháp. Khi mã nguồn phát triển quá nhanh, tôi dành vài lần nhắc nhở tiếp theo chỉ để làm bóng và cải thiện chất lượng mã. Điều này giữ cho mã nguồn được 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ứ. Có lẽ chúng ta không còn xa thời điểm viết ứng dụng web bằng C trở nên khả thi.