Leo de Moura, nhà sáng lập Lean và VP Distinguished Scientist tại AWS, vừa chia sẻ trong một buổi podcast với Ben Lorica về cách AI có thể thúc đẩy kiểm chứng hình thức (formal verification) trong phát triển phần mềm.
Lean là một ngôn ngữ lập trình kết hợp với một trợ lý chứng minh, cho phép người dùng viết mã đồng thời khai báo các tính chất mong muốn và chứng minh chúng bằng cách máy‑kiểm tra. Theo Leo, chỉ cần tin tưởng vào kernel của Lean – phần lõi kiểm tra chứng minh – thì mọi bằng chứng đều được xác thực, và hiện nay Lean đã có hai trình kiểm tra đã được xác minh, một trình thứ ba đang được phát triển.
AI tạo mã nhanh chóng, nhưng việc tin tưởng vào mã do AI sinh ra luôn gặp “bottleneck” về độ tin cậy. Kiểm chứng hình thức giúp khắc phục vấn đề này bằng cách cung cấp bằng chứng máy‑kiểm tra cho các thuộc tính quan trọng, thay vì chỉ dựa vào kiểm thử truyền thống. Leo cũng đề cập tới việc sử dụng Lean để tổng hợp mã có các tính chất nhất định, và khả năng xuất chứng minh ra các trình kiểm tra khác nhau để tăng cường độ tin cậy.
Cuối cùng, Leo dự đoán Lean sẽ trở thành công cụ quen thuộc trong cộng đồng AI trong năm tới, góp phần xây dựng một ngăn xếp phần mềm được xác minh toàn diện, đồng thời mở ra cơ hội mới cho các kỹ sư và nhà nghiên cứu tại Việt Nam.
Nguồn: Hacker News — Biên dịch & tổng hợp: danhbaai.com