Vitalik: Ngôn ngữ lập trình cao cấp mới đáng thử nên giúp người đọc dễ dàng hơn trong việc hiểu định nghĩa và định lý

Tin tức từ ChainCatcher, Vitalik đã đăng bài trên nền tảng X cho biết, một loại "ngôn ngữ lập trình cao cấp" mới đáng để thử nghiệm là ngôn ngữ được biên dịch thành Lean (hoặc HOL, v.v.), tập trung vào việc giúp con người dễ dàng đọc các định nghĩa và định lý nhất có thể. Thay vì chứng minh, vì chứng minh chỉ cần đúng là đủ, điều quan trọng nằm ở chính các định nghĩa và định lý. Mục đích dự kiến của nó là, AI xuất ra một đoạn chứng minh dài, trong khi người đọc cần hiểu những tuyên bố chính xác nào đã được chứng minh trong các đầu ra đó một cách dễ dàng nhất có thể.