Catala - DSL suy ra thuật toán trung thực từ văn bản pháp luật
(github.com/CatalaLang)- Catala là một ngôn ngữ đặc thù miền nhằm suy ra các thuật toán faithful-by-construction từ văn bản lập pháp, đồng thời là ngôn ngữ lập trình được thiết kế cho lập trình văn chương trong lĩnh vực pháp luật xã hội và tài chính
- Sau khi tập hợp các tài liệu về cơ chế xã hội và tài chính cần triển khai như luật, nghị định thi hành, án lệ..., việc hiện thực được viết theo cách chú giải ý nghĩa của từng dòng trong mỗi điều khoản thành mã
- Trình biên dịch Catala có thể tạo ra phiên bản PDF của phần hiện thực mà luật sư có thể đọc từ mã đã hoàn thiện và được kiểm thử; đây là ngôn ngữ được thiết kế với sự cộng tác của chuyên gia pháp lý để họ có thể rà soát và chứng nhận tính chính xác
- Các khái niệm cốt lõi là definition-under-conditions và default logic, dựa trên A Logic for Statutes của giáo sư Sarah Lawsky; cấu trúc logic của ngôn ngữ mô phỏng cấu trúc logic của pháp luật
- Công cụ phát triển gồm tô sáng cú pháp cho nhiều trình soạn thảo văn bản, tiện ích mở rộng VSCode, máy chủ LSP chuyên dụng, điều hướng mã, tự động hoàn thành, UX cho bộ kiểm thử và bộ định dạng
catala-format - Có thể học và tra cứu qua Catala book, Catala tutorial, cheat sheet ngữ pháp tiếng Pháp và tiếng Anh, cùng tài liệu trình biên dịch của phiên bản
mastermới nhất - Trình biên dịch và mã trong kho được phát hành theo Apache license version 2, trừ khi có giấy phép khác được ghi rõ ở các thư mục con
- Catala là một dự án nghiên cứu của Inria, và trình biên dịch hiện vẫn chưa ổn định, còn thiếu một số tính năng
1 bình luận
Ý kiến trên Hacker News
Dự án này dường như ngầm giả định rằng việc đặc tả hình thức các điều khoản pháp luật, và một hệ thống có thể diễn giải luật pháp phần lớn theo cách máy móc, là điều tốt
Hơn nữa, điều đó đồng nghĩa với việc xem hệ thống diễn giải hiện tại của con người, vốn có sự tùy nghi và biên độ sai số, là một vấn đề cần vượt qua. Tôi không hoàn toàn phản đối giả định đó, nhưng cũng không rõ nó có đúng hay không, và dường như các tác giả cũng chưa đưa ra lập luận để củng cố cho nó
Từ góc nhìn của người hiểu quá trình chuyển luật thành mã, tôi có thể hiểu việc dự án này muốn làm, ngay cả khi giá trị của nó chỉ giới hạn ở việc đem lại sự rõ ràng cho các nhà phát triển phần mềm
Tôi nghĩ điều này cũng liên quan mật thiết đến nhà nước pháp quyền. Theo https://www.britannica.com/topic/rule-of-law, luật phải công khai và rõ ràng, có hình thức chung và khả năng áp dụng phổ quát, chứa các yêu cầu xác định để mọi người có thể tham chiếu trước khi hành động, và nghĩa vụ pháp lý không được tạo ra một cách hồi tố. Tôi tự hỏi lợi ích của luật mơ hồ là gì
Khi học bằng luật, với tư cách là lập trình viên tôi đã khá quan tâm đến lĩnh vực này, và phát hiện có một cộng đồng lớn trong khối Pháp ngữ làm các công việc mang tính pháp trị như vậy. Vị giáo sư ở trường tôi quan tâm đến hướng này cũng có vẻ nghiêng về phía ảnh hưởng đó
Trong vài năm tôi đã cố thuyết phục một người bạn luật sư rằng giá mà có đúng thứ như thế này thì tốt, hóa ra có lẽ nó đã tồn tại từ lâu rồi
Tôi nghĩ nó thật sự tuyệt. Mọi luật nên được viết bằng ngôn ngữ như vậy, và được công khai với tô sáng cú pháp cùng các quy tắc định dạng nhất quán. Sau đó nên đưa việc học ngôn ngữ pháp luật này vào chương trình giáo dục ở trường. Khi đó khả năng mọi người đọc luật và tự tin vào cách hiểu của mình sẽ được cải thiện rất nhiều, và xã hội cũng sẽ được lợi lớn
Luật trong thực tế vốn đã được viết bằng ngôn ngữ tương đối bình thường, và từ ngữ hầu như luôn mang nghĩa như trong tiếng Anh thông dụng. Vấn đề là bản thân các khái niệm pháp lý mà những từ đó mô tả thì phức tạp, và thường đan xen các tham chiếu đến những luật, quy định, án lệ khác, v.v.
Đồng thời cũng có những trường hợp luật được pháp điển hóa, như Uniform Commercial Code. Tức là những trường hợp viết lại án lệ pháp một cách nhất quán, hợp nhất và sắp xếp các bản vá
Sẽ rất thú vị nếu “đan” cả các ca kiểm thử vào cùng. Bề mặt tiếp xúc nơi các mệnh đề logic chạm nhau chính là chỗ lỗi lọt vào
Đặc biệt là quanh các sự kiện theo thời gian; điều này dẫn đến mô hình hình thức, và cũng kéo theo nhiều lỗi hơn. Thông thường nếu có quy tắc về một khóa thì cần ít nhất ba kiểm thử¹: trường hợp lớn hơn, bằng, và nhỏ hơn. Nếu không có kiểu dữ liệu, v.v. thì cũng cần đầu vào âm, null, và các biên giá trị lớn nhất/nhỏ nhất
Ví dụ có thể đặt kiểm thử dựa trên dòng thời gian như “khi quy định được thông qua sau 3 tháng, các bên không còn được thực hiện B, nhưng dù vậy vẫn có ‘17 tấn’ chất thải bị đổ…”. Nếu có tích hợp bộ kiểm tra mô hình thì sẽ rất hữu ích. Lập pháp được xác minh hình thức, hoặc ít nhất là một pipeline kiểu DevOps cho quá trình mã hóa ngôn ngữ thành code, cũng có thể khả thi
¹ https://en.m.wikipedia.org/wiki/Equivalence_partitioning
Nhiều luật chứa rất nhiều cách diễn đạt đa nghĩa. Quy định gần đây của EU về việc có cho phép xe Nga hay không là một ví dụ hay. Tuy vậy, khi cố “số hóa” luật thành ngôn ngữ lập trình, đây có thể là một ý tưởng tốt để tìm ra mọi khả năng đa nghĩa hoặc định nghĩa mơ hồ
Tương tự như việc cố chứng minh bằng unit/integration/end-to-end test để thuyết phục reviewer rằng code hoạt động. Tức là đưa kiểm thử đầu-cuối vào hệ thống pháp luật
Tiến thêm một bước, ta còn có thể viết một bộ kiểm thử rồi tự động sinh ra phạm vi luật khả dĩ thỏa mãn các kiểm thử đó
Muốn thấy thêm định dạng bộ kiểm thử chuẩn để nêu rõ ý định của luật
Ở bang tôi từng sống trước đây, có một đề xuất luật cấm nội dung khiêu dâm trẻ em rất đơn giản với ý định tốt, nhưng nó quá đơn giản. Đại khái là “người nào gửi ảnh nhạy cảm của trẻ vị thành niên bằng điện thoại di động thì phạm tội truyền bá nội dung khiêu dâm trẻ em”, được viết bằng ngôn ngữ pháp lý nhưng cũng không chi tiết hơn thế nhiều. Tôi gọi cho người đề xuất dự luật và hỏi rằng nếu cô con gái giả định của tôi tự gửi ảnh khỏa thân của mình cho bạn trai thì chẳng phải theo luật mới nó sẽ trở thành trọng phạm sao; phản ứng là “Ôi trời, ý tôi không phải vậy!”, và cuối cùng họ rút dự luật để viết lại
Có thể tưởng tượng việc xử lý nó như mã chương trình và gắn các bài kiểm thử kiểu “luật này không áp dụng khi trẻ vị thành niên gửi ảnh của chính mình”. Điều đó buộc nhà lập pháp phải làm rõ ý định, và nếu họ nói “chúng tôi sẽ không dùng luật an toàn trẻ em trực tuyến để cấm nội dung thân thiện với người chuyển giới” thì có thể đáp “tốt, hãy đưa điều đó vào làm test case”. Trở ngại mang tính quyết định là các chính trị gia không thích bị đóng đinh rõ ràng như vậy
Nó cũng giúp viết luật phản ánh ý định dễ hơn, và các tòa án trong tương lai có thể dùng để đánh giá ý định của luật. Dù về mặt câu chữ luật có thể áp dụng cho trường hợp một thiếu niên 15 tuổi gửi selfie, nếu bài kiểm thử nêu rõ rằng đó không phải ý định thì có thể được tuyên vô tội. Có lẽ là bất khả thi vì hàng trăm lý do, nhưng vẫn có thể mơ tới
Tức là không phải kiểu cố tình viết luật mơ hồ để phạm vi bao trùm rộng rồi để mọi người tự tranh cãi ở tòa
Luật không cần phải có khả năng chạy được trên máy tính. Vì luật liên quan đến ý định và cách diễn giải ý định đó, nên bản thân bộ kiểm thử về thực chất cũng là một phần của luật, cứ đưa thẳng vào luật là được
Cá nhân tôi sẽ hài lòng nếu bất kỳ quốc gia nào cũng đính kèm mục đích lập pháp vào chính văn bản luật. Nếu có thể thì thêm cả các chỉ số hiệu quả chính để xem nó có hoạt động hay không cũng tốt. Về sau có thể đánh giá lại xem luật có thực sự vận hành, có gây tác dụng ngược, hay các trường hợp áp dụng chính có khác với lý do ban đầu khi ban hành hay không
[1] https://www.aclu.org/news/juvenile-justice/minnesota-prosecu...
Một thứ tương tự có tên Legal Logic xuất hiện thoáng qua trong cuốn Moving Mars (1993) của Greg Bear. Người Sao Hỏa là con người dùng nó với sự hỗ trợ của AI khi xây dựng luật cho xã hội mới giành độc lập của họ
Greg Bear là một tác giả khoa học viễn tưởng nổi tiếng đã qua đời chưa đầy một năm trước, và cáo phó của ông khi đó cũng được thảo luận ở đây. Ông là một trong những tác giả có ảnh hưởng lớn đến tuổi thiếu niên của tôi, nên tôi nhớ yếu tố này trong Moving Mars đặc biệt kích thích trí tưởng tượng, và tôi muốn đọc xem Catala cung cấp điều gì
[1] https://en.wikipedia.org/wiki/Greg_Bear
[2] https://en.wikipedia.org/wiki/Moving_Mars
[3] https://news.ycombinator.com/item?id=33679668
[4] https://news.ycombinator.com/item?id=33675708
Có một bài báo mô tả ngôn ngữ này: https://hal.inria.fr/hal-03159939. Cũng có một video tóm tắt ngắn: https://youtu.be/OiaFTFSAa1I
Lập trình viên thích đề xuất dùng thứ gì đó giống “ngôn ngữ lập trình” cho luật
Nhưng điều này bỏ qua rằng sự mơ hồ, theo một số nghĩa, là một phần quan trọng mang tính nền tảng của luật. Bởi bản thân thế giới, theo một số nghĩa, vốn mơ hồ về mặt nền tảng, và theo một số nghĩa khác thì lại được phân chia rõ ràng. Tất nhiên không phải loại mơ hồ nào cũng đáng mong muốn
Tuy nhiên, nếu “code là luật” thì tôi nghĩ cách khai thác kẽ hở sẽ còn tệ hơn. Thậm chí, nhiều luật nên tập trung nhiều hơn vào các giá trị cần được bảo vệ hơn là chi tiết triển khai, và điều đó về bản chất không thể rõ ràng bằng, mà sẽ mơ hồ hơn
Tôi sẽ không tranh luận đây là vấn đề của luật hay của việc thực thi, nhưng dù sao xã hội của chúng ta cũng được xây dựng trên sự mơ hồ và thực thi không đồng đều
value.fair_markettrong phần concepts [0]. Luật sư có thể tranh luận về ý nghĩa của nó, nhưng các định nghĩa cạnh tranh cũng có thể được định nghĩa bằng chương trìnhTôi đồng ý rằng sự quan tâm đối với luật nên hướng vào kết quả hơn là chi tiết triển khai. Để làm vậy, cần có cách tạo ra các hàm đánh giá để đo lường kết quả của luật mới, và những hệ thống như Catala có thể giúp mô hình hóa kết quả kỳ vọng và lựa chọn giữa các dự luật cạnh tranh. Ví dụ nếu kết quả là “muốn giảm ô nhiễm” thì chính sách có thể là “cấm ngành công nghiệp gây ô nhiễm” hoặc “đánh thuế ngoại tác ô nhiễm”; cả hai đều tạo ra những hệ quả phức tạp, nên phân tích tự động và đo lường thực nghiệm sẽ tốt hơn
[0] https://github.com/CatalaLang/catala#concepts
Tôi không chắc liệu có vấn đề nào lớn cần được giải quyết để máy tính thực sự suy luận về câu chữ pháp luật hay không. Phần phức tạp là cân nhắc tính công bằng, và điều đó vẫn cần con người và luật sư
Tôi tò mò liệu có nhà lập pháp, luật sư hay thẩm phán nào kỳ vọng vào thứ này không, hay chỉ có các lập trình viên kỳ vọng
Tôi không tin tưởng hệ thống pháp luật của chúng ta lắm. Không hiểu sao bạn lại hỏi
Với tư cách là người nói tiếng Catalan, tôi thấy việc trùng tên với ngôn ngữ được nói đến trong bài là rất đáng tiếc
Việc chọn tên thật sự đáng tiếc. Nó giống như đặt tên một ngôn ngữ lập trình là “français”, “Deutsch”, hoặc “English” vậy
Ở phần dưới của readme có ghi “ngôn ngữ này được đặt theo tên Pierre Catala”. Tôi đề xuất đổi thành PierreLang thì hơn
Là người bản ngữ Catalan, tôi cũng khá ngạc nhiên khi thấy cái tên này, nhưng nếu đó là một họ phổ biến thì cũng hợp lý