Catala - DSL สำหรับสกัดอัลกอริทึมที่สอดคล้องกับข้อความกฎหมาย
(github.com/CatalaLang)- Catala เป็นภาษาเฉพาะโดเมนสำหรับสกัด อัลกอริทึมแบบ faithful-by-construction จากข้อความกฎหมาย และเป็นภาษาโปรแกรมที่ออกแบบมาสำหรับการทำ literate programming ของกฎหมายด้านสังคมและการคลัง
- การพัฒนาทำโดยรวบรวมเอกสารเกี่ยวกับกลไกทางสังคมและการคลังที่ต้องการนำไปใช้งานจริง เช่น กฎหมาย กฎกระทรวง และคำพิพากษา แล้วเขียน implementation ในลักษณะที่ใส่คำอธิบายแต่ละบรรทัดของแต่ละมาตราเป็นคอมเมนต์ในโค้ด
- คอมไพเลอร์ของ Catala สามารถสร้าง implementation ในรูปแบบ PDF version ที่ทนายความอ่านได้จากโค้ดที่ทำเสร็จและผ่านการทดสอบแล้ว และภาษานี้ถูกออกแบบโดยร่วมมือกับผู้เชี่ยวชาญด้านกฎหมายเพื่อให้ผู้เชี่ยวชาญด้านกฎหมายตรวจทานและรับรองความถูกต้องได้
- แนวคิดหลักคือ definition-under-conditions และ default logic ซึ่งอิงจาก A Logic for Statutes ของศาสตราจารย์ Sarah Lawsky โดยโครงสร้างตรรกะของภาษาจะเลียนแบบโครงสร้างตรรกะของกฎหมาย
- เครื่องมือพัฒนาประกอบด้วยการเน้นไวยากรณ์สำหรับโปรแกรมแก้ไขข้อความหลายตัว, ส่วนขยาย VSCode, LSP server เฉพาะทาง, การนำทางโค้ด, การเติมโค้ดอัตโนมัติ, UX ของ test suite และตัวจัดรูปแบบ
catala-format - การเรียนรู้และเอกสารอ้างอิงเข้าถึงได้ผ่าน Catala book, Catala tutorial, cheat sheet ไวยากรณ์ภาษาฝรั่งเศสและอังกฤษ และ เอกสารคอมไพเลอร์ ของเวอร์ชัน
masterล่าสุด - คอมไพเลอร์และโค้ดในรีโพซิทอรีเผยแพร่ภายใต้ Apache license version 2 เว้นแต่จะมีการระบุไลเซนส์แยกต่างหากไว้ในไดเรกทอรีย่อย
- Catala เป็นโครงการวิจัยของ Inria และคอมไพเลอร์ยังไม่เสถียรนัก โดยยังขาดฟีเจอร์บางส่วน
1 ความคิดเห็น
ความคิดเห็นบน Hacker News
โปรเจกต์นี้ดูเหมือนจะตั้งสมมติฐานโดยนัยว่า การระบุบทบัญญัติกฎหมายอย่างเป็นรูปแบบ และการมีระบบที่ตีความกฎหมายได้โดยอาศัยกลไกเป็นส่วนใหญ่ เป็นสิ่งที่ดี
ยิ่งไปกว่านั้น เท่ากับมองว่าระบบผู้ตีความที่เป็นมนุษย์ในปัจจุบัน ซึ่งมีดุลยพินิจและช่วงความคลาดเคลื่อน เป็นปัญหาที่ต้องเอาชนะ แม้ผมไม่ได้คัดค้านสมมติฐานนั้นโดยสิ้นเชิง แต่ก็ยังไม่ชัดว่าถูกต้องหรือไม่ และดูเหมือนผู้เขียนก็ไม่ได้เสนอเหตุผลสนับสนุนไว้
ในฐานะคนที่รู้กระบวนการแปลงกฎหมายเป็นโค้ด ต่อให้คุณค่าของมันจำกัดอยู่แค่การให้ความชัดเจนแก่ผู้พัฒนาซอฟต์แวร์ ก็ยังเข้าใจได้ว่าโปรเจกต์นี้พยายามทำอะไร
ผมคิดว่านี่เกี่ยวข้องอย่างใกล้ชิดกับหลักนิติธรรมด้วย ตาม https://www.britannica.com/topic/rule-of-law กฎหมายควรเปิดเผย ชัดเจน มีรูปแบบทั่วไปและใช้ได้อย่างเป็นสากล มีข้อกำหนดที่แน่นอนให้ผู้คนอ้างอิงได้ก่อนลงมือกระทำ และไม่ควรสร้างภาระผูกพันทางกฎหมายย้อนหลัง ผมสงสัยว่ากฎหมายที่คลุมเครือมีข้อดีอะไร
ตอนเรียนปริญญานิติศาสตร์ ในฐานะโปรแกรมเมอร์ผมสนใจสาขานี้มาก และพบว่ามีชุมชนใหญ่ในโลกภาษาฝรั่งเศสที่ทำงานแนว legalistic แบบนี้ อาจารย์ในมหาวิทยาลัยของผมที่สนใจเรื่องนี้ก็ดูเหมือนจะเอนเอียงไปทางอิทธิพลสายนั้นเช่นกัน
ผมพยายามโน้มน้าวเพื่อนทนายมาหลายปีแล้วว่าอยากให้มีของแบบนี้พอดี แต่กลายเป็นว่ามันน่าจะมีอยู่มาตลอด
ผมคิดว่ามันเจ๋งมาก กฎหมายทั้งหมดควรถูกเขียนด้วยภาษาลักษณะนี้ และเผยแพร่พร้อม syntax highlighting กับกฎการจัดรูปแบบที่สม่ำเสมอ จากนั้นควรบรรจุการเรียนภาษากฎหมายนี้ไว้ในหลักสูตรของโรงเรียนด้วย แบบนั้นความสามารถของผู้คนในการอ่านกฎหมายและมั่นใจในความเข้าใจของตัวเองจะดีขึ้นมาก และจะเป็นประโยชน์ใหญ่ต่อสังคม
กฎหมายในโลกจริงเขียนด้วยภาษาที่ค่อนข้างธรรมดาอยู่แล้ว และคำต่าง ๆ แทบทุกครั้งก็มีความหมายเหมือนในภาษาอังกฤษทั่วไป ปัญหาคือแนวคิดทางกฎหมายที่คำเหล่านั้นอธิบายต่างหากที่ซับซ้อน และมักพันเกี่ยวกับการอ้างอิงกฎหมาย ระเบียบ และคำพิพากษาอื่น ๆ
ขณะเดียวกันก็มีกฎหมายที่ถูกประมวลไว้เป็นลายลักษณ์อักษรอย่าง Uniform Commercial Code เช่นกัน กล่าวคือเป็นกรณีที่นำกฎหมายจากคำพิพากษามาเขียนใหม่ให้สอดคล้องกัน และรวมแพตช์เข้าด้วยกันอย่างเป็นระเบียบ
ถ้า “สอดแทรก” test case เข้าไปด้วยก็น่าสนใจ พื้นผิวสัมผัสที่ประโยคเชิงตรรกะมาบรรจบกันนี่แหละคือจุดที่บั๊กจะเล็ดลอดเข้าไป
โดยเฉพาะบริเวณเหตุการณ์ตามเวลา ซึ่งจะนำไปสู่ formal model และบั๊กก็จะมากขึ้นด้วย โดยทั่วไปถ้ามีกฎเกี่ยวกับคีย์ อย่างน้อยต้องมีการทดสอบสามแบบ¹: กรณีมากกว่า เท่ากัน และน้อยกว่า ถ้าไม่มี type อะไรแบบนั้น ก็ต้องทดสอบ input ติดลบ, null, และขอบเขตค่าสูงสุด/ต่ำสุดด้วย
เช่น อาจมีการทดสอบตามไทม์ไลน์อย่าง “เมื่อข้อบังคับผ่านในอีก 3 เดือนต่อมา และคู่กรณีไม่สามารถใช้สิทธิ B ได้แล้ว แต่ก็ยังมีการทิ้งของเสีย ‘17 ตัน’ …” ถ้ามี model checker รวมเข้ามาด้วยจะช่วยได้มาก อาจถึงขั้นมีการออกกฎหมายที่ผ่านการ formal verification หรืออย่างน้อยก็มี pipeline แบบ DevOps สำหรับกระบวนการเข้ารหัสภาษาเป็นโค้ด
¹ https://en.m.wikipedia.org/wiki/Equivalence_partitioning
กฎหมายจำนวนมากมีถ้อยคำกำกวมอยู่มาก กฎระเบียบ EU ล่าสุดเกี่ยวกับว่าจะอนุญาตรถรัสเซียหรือไม่เป็นตัวอย่างที่ดี อย่างไรก็ดี ตอนพยายาม “ทำให้กฎหมายเป็นดิจิทัล” ในรูปภาษาโปรแกรม นี่อาจเป็นไอเดียที่ดีในการค้นหาความกำกวมหรือนิยามที่คลุมเครือทั้งหมดที่เป็นไปได้
คล้ายกับการพยายามพิสูจน์ให้ reviewer เชื่อว่าโค้ดทำงานได้ด้วย unit/integration/end-to-end test เท่ากับมีend-to-end testให้ระบบกฎหมายด้วย
ก้าวไปอีกขั้น อาจเขียนชุดทดสอบ แล้วสร้างขอบเขตกฎหมายที่เป็นไปได้ซึ่งผ่านชุดทดสอบนั้นโดยอัตโนมัติ
อยากเห็น รูปแบบชุดทดสอบมาตรฐาน ที่ระบุเจตนารมณ์ของกฎหมายมากกว่านี้
รัฐที่ผมเคยอยู่ก่อนหน้านี้เคยเสนอร่างกฎหมายห้ามสื่อลามกเด็กที่มีเจตนาดีและเรียบง่ายมาก แต่กลับเรียบง่ายเกินไป โดยคร่าว ๆ คือ “ผู้ใดส่งภาพโจ่งแจ้งของผู้เยาว์ทางโทรศัพท์มือถือ มีความผิดฐานส่งต่อสื่อลามกเด็ก” อะไรทำนองนั้น แม้จะเขียนด้วยภาษากฎหมาย แต่ก็ไม่ได้ละเอียดไปกว่านี้มากนัก ผมโทรไปถามผู้เสนอร่างกฎหมายว่า ถ้าลูกสาวสมมติของผมส่งรูปเปลือยของตัวเองให้แฟน เธอจะกลายเป็นอาชญากรความผิดร้ายแรงตามกฎหมายใหม่นี้ใช่ไหม เขาก็ตอบประมาณว่า “อ้าว แย่แล้ว เราไม่ได้หมายความแบบนั้น!” และสุดท้ายก็ถอนร่างกฎหมายกลับไปเขียนใหม่
ลองจินตนาการว่าปฏิบัติกับมันเหมือนโค้ดโปรแกรม แล้วใส่เทสต์อย่าง “กฎหมายนี้ไม่ใช้บังคับในกรณีที่ผู้เยาว์ส่งรูปของตนเอง” ลงไปได้ วิธีนี้จะบังคับให้ผู้ออกกฎหมายต้องทำให้เจตนาชัดเจน และถ้าบอกว่า “เราจะไม่ใช้กฎหมายความปลอดภัยเด็กออนไลน์ไปห้ามเนื้อหาที่สนับสนุนคนข้ามเพศ” ก็พูดได้ว่า “ดี งั้นใส่เป็นเทสต์เคสไว้เลย” อุปสรรคสำคัญคือ นักการเมืองไม่ชอบการถูกตรึงไว้อย่างนั้น
อีกทั้งจะทำให้การเขียนกฎหมายที่สะท้อนเจตนาง่ายขึ้น และศาลในอนาคตใช้ประเมินเจตนารมณ์ของกฎหมายได้ ต่อให้ตามถ้อยคำแล้วกรณีเด็กอายุ 15 ส่งเซลฟีจะเข้าข่าย แต่ถ้าเทสต์ระบุว่าไม่ใช่เจตนา ก็อาจตัดสินว่าไม่มีความผิดได้ คงเป็นไปไม่ได้ด้วยเหตุผลนับร้อย แต่ก็ฝันได้
กล่าวคือ ไม่ใช่การจงใจเขียนกฎหมายให้คลุมเครือเพื่อให้กินความกว้าง แล้วปล่อยให้ผู้คนไปต่อสู้กันในศาล
กฎหมายไม่จำเป็นต้องรันได้บนคอมพิวเตอร์ มันเป็นเรื่องของเจตนาและการตีความ ดังนั้นชุดทดสอบเองก็แทบจะเป็นส่วนหนึ่งของกฎหมายอยู่แล้ว แค่ใส่ไว้ในกฎหมายก็พอ
โดยส่วนตัวแล้ว ผมคงพอใจถ้าประเทศไหนก็ตามแนบ เจตนารมณ์ของกฎหมาย ไว้กับตัวกฎหมายเอง ถ้าเป็นไปได้ก็อยากให้แนบตัวชี้วัดผลสำเร็จหลักเพื่อดูว่ามันทำงานหรือไม่ด้วย ภายหลังจะได้ประเมินซ้ำได้ว่ากฎหมายทำงานจริงหรือไม่ ให้ผลย้อนกลับหรือไม่ หรือกรณีการบังคับใช้หลัก ๆ แตกต่างจากเหตุผลที่เริ่มนำกฎหมายนั้นมาใช้หรือไม่
[1] https://www.aclu.org/news/juvenile-justice/minnesota-prosecu...
ในหนังสือ Moving Mars (1993) ของ Greg Bear มีสิ่งที่คล้ายกันปรากฏสั้น ๆ ในชื่อ Legal Logic ชาวอังคารที่เป็นมนุษย์ใช้มันด้วยความช่วยเหลือของ AI ตอนสร้างกฎหมายของสังคมที่เพิ่งได้รับเอกราช
Greg Bear เป็นนักเขียน SF ชื่อดังที่เสียชีวิตไปไม่ถึงหนึ่งปีก่อน และตอนนั้นที่นี่ก็มีการพูดคุยถึงข่าวมรณกรรมของเขา เขาเป็นหนึ่งในนักเขียนที่มีอิทธิพลอย่างมากต่อช่วงวัยรุ่นของผม เลยจำได้ว่าองค์ประกอบนี้ใน Moving Mars กระตุ้นจินตนาการเป็นพิเศษ และอยากอ่านดูว่า Catala มีอะไรให้บ้าง
[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
มีบทความวิชาการที่อธิบายภาษานี้: https://hal.inria.fr/hal-03159939 และมี วิดีโอสรุป สั้น ๆ ด้วย: https://youtu.be/OiaFTFSAa1I
โปรแกรมเมอร์ชอบเสนอให้ใช้สิ่งที่คล้าย “ภาษาโปรแกรม” กับกฎหมาย
แต่นี่พลาดประเด็นว่า ความคลุมเครือ ในบางแง่เป็นส่วนสำคัญเชิงรากฐานของกฎหมาย เพราะโลกเองในบางแง่ก็คลุมเครือโดยพื้นฐาน และในบางแง่ก็แบ่งแยกได้ชัดเจน แน่นอนว่าไม่ใช่ความคลุมเครือทุกชนิดที่พึงประสงค์
แต่ถ้า “โค้ดคือกฎหมาย” จริง ๆ ผมคิดว่าวิธีใช้ประโยชน์จากช่องโหว่จะแย่ลงกว่าเดิมเสียอีก กฎหมายจำนวนมากควรเน้นคุณค่าที่ต้องรักษามากกว่ารายละเอียดการนำไปปฏิบัติ ซึ่งโดยเนื้อแท้แล้วต้องชัดเจนน้อยกว่าและคลุมเครือมากกว่า
ผมจะไม่ถกเถียงว่านี่เป็นปัญหาของกฎหมายหรือของการบังคับใช้ แต่ไม่ว่าอย่างไร สังคมของเราก็ตั้งอยู่บน ความคลุมเครือและการบังคับใช้ที่ไม่สม่ำเสมอ
value.fair_marketในส่วน concepts [0] ทนายความอาจโต้แย้งกันได้ว่ามันหมายถึงอะไร แต่คำนิยามที่แข่งขันกันก็สามารถนิยามเป็นโปรแกรมได้เช่นกันผมเห็นด้วยว่าความสนใจต่อกฎหมายควรมุ่งไปที่ ผลลัพธ์ มากกว่ารายละเอียดการนำไปปฏิบัติ เพื่อทำเช่นนั้น เราต้องมีวิธีสร้างฟังก์ชันประเมินผลลัพธ์ของกฎหมายใหม่ และระบบอย่าง Catala อาจช่วยสร้างแบบจำลองผลลัพธ์ที่คาดหวังและช่วยเลือกท่ามกลางร่างกฎหมายที่แข่งขันกันได้ เช่น ถ้าผลลัพธ์คือ “อยากลดมลพิษ” นโยบายอาจเป็น “ห้ามอุตสาหกรรมที่ก่อมลพิษ” หรือ “เก็บภาษีผลกระทบภายนอกจากมลพิษ” ก็ได้ ซึ่งทั้งสองแบบให้ผลลัพธ์ที่ซับซ้อน ดังนั้นการวิเคราะห์อัตโนมัติและการวัดเชิงประจักษ์น่าจะดีกว่า
[0] https://github.com/CatalaLang/catala#concepts
ไม่แน่ใจว่ามีปัญหาอะไรที่คอมพิวเตอร์จะช่วยแก้ได้มากจริง ๆ ในการให้เหตุผลเกี่ยวกับถ้อยคำทางกฎหมาย ส่วนที่ซับซ้อนคือ การชั่งน้ำหนักความเป็นธรรม และเรื่องนี้ยังคงต้องอาศัยมนุษย์กับทนายความ
สงสัยว่ามีนักนิติบัญญัติ ทนายความ หรือผู้พิพากษาคนไหนคาดหวังสิ่งนี้อยู่ไหม หรือมีแต่โปรแกรมเมอร์เท่านั้นที่คาดหวัง
ผมไม่ค่อยเชื่อถือระบบกฎหมายของเราเท่าไร ไม่รู้ว่าถามทำไม
ในฐานะคนที่พูดภาษา Catalan รู้สึกว่า ชื่อชนกัน กับภาษาที่กล่าวถึงในบทความเป็นเรื่องน่าเสียดายมาก
การเลือกชื่อนี้น่าเสียดายจริง ๆ คล้ายกับการตั้งชื่อภาษาโปรแกรมว่า “français”, “Deutsch” หรือ “English”
ช่วงล่างของ readme เขียนว่า “ภาษานี้ตั้งชื่อตาม Pierre Catala” ผมขอเสนอว่าเปลี่ยนเป็น PierreLang ดีกว่า
ในฐานะเจ้าของภาษา Catalan ผมค่อนข้างตกใจเมื่อเห็นชื่อนี้ แต่ถ้าเป็นนามสกุลที่พบได้ทั่วไปก็สมเหตุสมผล