Lean: Ngôn ngữ lập trình có khả năng hoàn thiện đến mức hoàn hảo

Tại một bữa tiệc, tác giả Alok Singh đã liệt kê tên của 40 ngôn ngữ lập trình khác nhau, từ Racket, Agda, Clean, Elm, TypeScript cho đến C, C++ và Java. Tuy nhiên, ông khẳng định rằng Lean là ngôn ngữ tốt nhất trong số đó. Lý do không phải vì Lean đã hoàn hảo, mà vì nó là một ngôn ngữ có khả năng "hoàn thiện" (perfectable).

Khái niệm về khả năng "hoàn thiện"

Trong mọi ngôn ngữ lập trình, lập trình viên luôn mong muốn nói về chính mã nguồn của mình — ví dụ như khẳng định một hàm cụ thể luôn trả về một giá trị nhất định. Trong hầu hết các ngôn ngữ, bạn biết điều đó là đúng, nhưng ngôn ngữ không hỗ trợ bạn sử dụng sự thật đó một cách chính thức.

Với Lean, bạn có thể viết các thuộc tính về Lean ngay trong chính Lean. Tất cả các sự thật và thuộc tính này tạo nên sự tiến bộ. Ví dụ, hãy xem xét hàm returnFive:

def returnFive (x : Int) : Int := 5

Trong Lean, bạn có thể chứng minh (thông qua một định lý) rằng hàm này luôn trả về 5 bất kể đầu vào:

theorem returnFive_eq_five (x : Int) : returnFive x = 5 := rfl

Bạn thậm chí có thể sử dụng sự thật này để chứng minh các biểu thức toán học phức tạp hơn, nơi trình biên dịch hiểu và xác minh logic của bạn.

Hệ thống kiểu và Trình chứng minh định lý

Xu hướng chung của ngành công nghiệp phần mềm là chuyển sang các ngôn ngữ có kiểu dữ liệu (typed languages) mạnh mẽ hơn như TypeScript hay Rust. Ngay cả PHP và Python cũng bắt đầu thêm chú thích kiểu. Tuy nhiên, Lean đi xa hơn với "kiểu phụ thuộc" (dependent types).

Về bản chất, Lean là một trình chứng minh định lý (theorem prover). Bất kỳ ngôn ngữ phụ thuộc nào cũng có thể trở thành trình chứng minh định lý, nhưng Lean sở hữu cơ sở hạ tầng API tuyệt vời cho việc này. Nó cho phép bạn chứng minh hai kiểu dữ liệu bằng nhau hoặc khác nhau, tạo ra một nền tảng vững chắc cho phần ngữ nghĩa (semantics).

Metaprogramming mượt mà

Một nửa câu chuyện của Lean nằm ở phần cú pháp, nơi metaprogramming và cú pháp tùy chỉnh đóng vai trò then chốt. Trong khi nhiều ngôn ngữ có cơ chế macro khá vụng về, Lean lại hoạt động cực kỳ liền mạch.

Tác giả đưa ra ví dụ về việc tạo ra một bàn cờ Tic-Tac-Toe với cú pháp trực quan:

elab "board! " b:tttBoardSyntax : term => do
  -- Xử lý cú pháp tùy chỉnh để tạo bàn cờ tại thời điểm biên dịch

Bạn có thể định nghĩa cú pháp để bàn cờ trông như sau:

X | O | _
_ | X | _
O | _ | X

Khả năng này cho phép thiết kế API theo từng tầng lớp và ẩn sự phức tạp đằng sau các cú pháp tùy chỉnh. Việc thay đổi cách diễn giải cú pháp cũng trở nên dễ dàng hơn bao giờ hết.

Tối ưu hóa và Hiệu suất

Tốc độ luôn là một yếu tố quan trọng. Lean hiện tại có thể chưa nhanh bằng Rust, nhưng nó có trần tối ưu hóa rất cao nhờ khả năng chứng minh sự tương đương giữa hai đoạn mã.

Nếu hai hàm được chứng minh là bằng nhau trên mọi đầu vào, trình biên dịch có thể tự do thay thế cái này bằng cái khác để tối ưu hóa. Leo de Moura (nhà phát triển chính của Lean) cũng đang tập trung vào việc này, sẵn sàng hy sinh tính tương thích ngược để đạt được hiệu suất tốt hơn. Trong kỷ nguyên AI, việc viết lại mã nguồn trở nên dễ dàng hơn, và một trình chứng minh định lý chính là công cụ tái cấu trúc (refactoring) tối thượng.

Cộng đồng đang phát triển

Cuối cùng, Lean là ngôn ngữ duy nhất trong phân khúc này thực sự đang thu hút sự chú ý. Các đối thủ như Coq, Idris, Agda hay F* không còn cạnh tranh mạnh mẽ hoặc không đạt được khối lượng người dùng quan trọng. Lean là ngôn ngữ kết hợp khả năng lập trình thực thụ với khả năng chứng minh định lý, và cộng đồng của nó đang ngày càng lớn mạnh.