Tin tức TechFlow, ngày 21 tháng 7, theo như Vitalik Buterin(@VitalikButerin)đăng bài cho biết, ông đề xuất phát triển một loại ngôn ngữ lập trình cấp cao mới, ngôn ngữ này có thể biên dịch thành Lean(hoặc các công cụ xác minh hình thức như HOL), mục tiêu cốt lõi là giúp con người đọc nội dung định nghĩa và định lý một cách dễ dàng nhất có thể(chứ không phải bản thân chứng minh). Kịch bản sử dụng dự kiến của ông là: AI chịu trách nhiệm xuất ra nội dung chứng minh, còn ngôn ngữ này sẽ giúp độc giả nhanh chóng hiểu các mệnh đề cụ thể mà AI đã chứng minh.
Chuyên sâu báo cáo Web3
Tôi muốn đăng bài
Yêu cầu phỏng vấn
Theo dõi chúng tôi
Cảnh báo rủi ro: mọi nội dung trên website này không cấu thành tư vấn đầu tư và chúng tôi không cung cấp bất kỳ dịch vụ tín hiệu hay dẫn dắt giao dịch nào. Theo thông báo của PBoC và 10 bộ ngành về việc tăng cường phòng ngừa rủi ro đầu cơ tiền mã hóa, xin hãy nâng cao ý thức rủi ro. Liên hệ: [email protected] Mã ICP: 琼ICP备2022009338号




