วิธีเชิงรูปนัยและอนาคตของการเขียนโปรแกรม
(blog.janestreet.com)- วิธีเชิงรูปนัย คือเครื่องมือที่ใช้พิสูจน์ว่าซอฟต์แวร์มีคุณสมบัติตามที่ตั้งใจไว้หรือไม่ และเมื่อการเขียนโค้ดด้วยเอเจนต์แพร่หลาย การประเมินต้นทุนต่อประโยชน์ก็กำลังเปลี่ยนไป
- ในอดีต Jane Street มองว่าวิธีเชิงรูปนัยมีความคุ้มค่าต่อต้นทุนต่ำ ยกเว้นบางกรณีเฉพาะทาง แต่ตอนนี้กำลังสร้าง ทีมเฉพาะทาง ขึ้นมา
- seL4 ใช้เวลาถึง 25 คน-ปีในการตรวจพิสูจน์โค้ด C จำนวน 8,700 บรรทัด และต้องใช้บทพิสูจน์ราว 23 บรรทัดต่อโค้ด 1 บรรทัด พร้อมเวลาตรวจพิสูจน์ประมาณครึ่งคน-วันต่อ 1 บรรทัด
- โค้ดที่เอเจนต์สร้างขึ้นยังต่างจากคุณภาพระดับพร้อมปล่อยใช้งานจริง และวิธีเชิงรูปนัยกำลังมีความสำคัญมากขึ้นในฐานะเครื่องมือเพื่อลด คอขวดด้านการตรวจพิสูจน์ และให้ฟีดแบ็กที่ทรงพลังแก่เอเจนต์
- Jane Street มองว่าตนสามารถควบคุมภาษาได้อย่างลึกซึ้ง และมี ชุมชนนักพัฒนาที่พร้อม จึงมีโอกาสพัฒนา OxCaml ควบคู่ไปกับแนวทางที่ยึดการพิสูจน์เป็นศูนย์กลาง
วิธีเชิงรูปนัยและอนาคตของการเขียนโปรแกรม
- ตลอด 25 ปีที่ผ่านมา Jane Street พูดมาโดยตลอดว่าในระดับองค์กรพวกเขาไม่ได้สนใจ วิธีเชิงรูปนัย แต่ตอนนี้ไม่ได้ยึดจุดยืนนั้นอีกต่อไป
- พวกเขาให้ความสำคัญกับพลังของเครื่องมือสำหรับเขียนโค้ดให้ดีขึ้นและน่าเชื่อถือยิ่งขึ้นมาโดยตลอด และมองว่าระบบชนิดข้อมูลเป็นวิธีเชิงรูปนัยแบบเบาที่ให้ประโยชน์อย่างมาก
- ยกเว้นกรณีเฉพาะทาง โดยเฉพาะการสังเคราะห์ฮาร์ดแวร์ พวกเขาเคยตัดสินว่าวิธีเชิงรูปนัยมีต้นทุนสูงเกินไปจนไม่เหมาะกับซอฟต์แวร์ส่วนใหญ่
- seL4 เป็นไมโครเคอร์เนลที่ผ่านการพิสูจน์เชิงรูปนัยและเป็นความสำเร็จที่สำคัญ แต่การตรวจพิสูจน์โค้ด C จำนวน 8,700 บรรทัดใช้เวลาถึง 25 คน-ปี
- ต้องใช้บทพิสูจน์ประมาณ 23 บรรทัดต่อโค้ด 1 บรรทัด และต้องใช้เวลาราวครึ่งคน-วันเพื่อพิสูจน์โค้ด 1 บรรทัด
- สำหรับกรณีที่มีความเสี่ยงสูงและมีสเปกค่อนข้างชัดเจน เช่น ไมโครเคอร์เนลที่เกี่ยวข้องกับความปลอดภัย วิธีนี้อาจมีคุณค่า
- แต่มันไม่เหมาะกับซอฟต์แวร์ส่วนใหญ่ และพวกเขารู้สึกว่ามันไม่เหมาะแม้แต่กับซอฟต์แวร์ที่สำคัญที่สุดของ Jane Street เอง
- การมาถึงของการเขียนโค้ดด้วยเอเจนต์ทำให้การประเมินนี้เปลี่ยนไป และความสงสัยต่อศักยภาพของวิธีเชิงรูปนัยก็เปลี่ยนเป็นความคาดหวัง
- Jane Street กำลังตั้ง ทีมวิธีเชิงรูปนัย และหวังว่าจะทำให้มันเป็นเครื่องมือสร้างซอฟต์แวร์ที่มีประโยชน์กว้างขวางพอ ๆ กับระบบชนิดข้อมูลที่ซับซ้อน
ทำไมถึงเปลี่ยนใจ
- การเขียนโค้ดด้วยเอเจนต์กำลังสั่นคลอนสมดุลต้นทุนต่อประโยชน์เดิมของ วิธีเชิงรูปนัย ในหลายด้าน
- นี่ไม่ได้หมายความว่าเอเจนต์จะสามารถประกอบบทพิสูจน์ยาก ๆ ขึ้นมาเองได้โดยลำพัง แต่โมเดลช่วยได้มาก และทำให้ผู้คนจำนวนมากขึ้นใช้เครื่องมือเหล่านี้ได้อย่างมีประสิทธิผล
- เมื่อการใช้วิธีเชิงรูปนัยง่ายขึ้นกว่าก่อน จึงคุ้มที่จะกลับมาทบทวนการคำนวณความคุ้มค่าต่อค่าใช้จ่ายแบบเดิม
-
คอขวดด้านการตรวจพิสูจน์สำคัญมากขึ้น
- โมเดลเขียนโค้ดที่มีประโยชน์ได้ดีขึ้นเรื่อย ๆ แต่ยังมีช่องว่างขนาดใหญ่ระหว่างโค้ดที่โมเดลสร้างกับโค้ดที่พร้อมปล่อยใช้งานจริง
- โมเดลเก่งอย่างน่าทึ่งในการบรรลุเป้าหมายที่ได้รับ แต่ยังไม่แข็งแกร่งพอในการรักษาหรือยกระดับคุณภาพของโค้ดเบสระหว่างทาง
- โค้ดที่เอเจนต์สร้างกำลังดีขึ้นก็จริง แต่ยังมักซับซ้อนเกินจำเป็น มีบั๊กประหลาดและกรณีขอบจำนวนมาก และมักไม่ทำตามอินวาเรียนต์หลักของโค้ดเบส
- มนุษย์ต้องใช้เวลามากในการตรวจว่าคุณภาพของโค้ดที่เอเจนต์สร้างนั้นดีพอหรือไม่
- วิธีเชิงรูปนัยสามารถลด ภาระในการตรวจพิสูจน์ นี้ และทำให้กระบวนการรีวิวมีประสิทธิภาพมากขึ้น
-
เอเจนต์แข็งแกร่งขึ้นจากฟีดแบ็ก
- เอเจนต์ได้ประโยชน์จาก ฟีดแบ็ก ทั้งตอนฝึกด้วยการเรียนรู้แบบเสริมกำลังและตอนนำมาใช้เขียนโค้ด
- วิธีเชิงรูปนัยเป็นรูปแบบฟีดแบ็กที่ทรงพลัง ซึ่งช่วยเพิ่มความสามารถของเอเจนต์ในการแก้ปัญหาที่ยาก
- การทดสอบก็มีคุณค่ามากเช่นกัน และจะยิ่งดีขึ้นเมื่อใช้ การทดสอบเชิงคุณสมบัติ และ fuzzing
- แต่การทดสอบอย่างเดียวไม่เพียงพอ และมีข้อจำกัดโดยเนื้อแท้ในการครอบคลุม state space ที่โปรแกรมสามารถสำรวจได้
- จากประสบการณ์การเขียนโปรแกรมด้วย OxCaml เอเจนต์ได้ประโยชน์อย่างมากจาก การรับประกันแบบครอบจักรวาล ที่ระบบชนิดข้อมูลมอบให้
- ถ้าระบบชนิดข้อมูลสามารถป้องกัน data race ได้ ก็สามารถกำจัด data race ออกไปได้
- หากออกแบบชนิดข้อมูลให้ดีจนทำให้ช่องโหว่ cross-site scripting เป็นไปไม่ได้ ก็สามารถกำจัดช่องโหว่นั้นได้ในแบบที่การทดสอบธรรมดาทำได้ยาก
- ชนิดข้อมูลช่วยบรรเทาคอขวดด้านการตรวจพิสูจน์และให้ฟีดแบ็กที่ดีกว่าเมื่อต้องเขียนโปรแกรมร่วมกับเอเจนต์
- และหากใช้เทคนิคการพิสูจน์ที่ทรงพลังยิ่งขึ้น ก็ยังมีช่องทางให้ปรับปรุงได้อีก
ทำไมต้องทำที่นี่
- ทั่วโลกกำลังคิดกันว่าเอเจนต์มีความหมายอย่างไรต่ออนาคตของการเขียนโปรแกรม และก็มีสตาร์ตอัปจำนวนมากที่พยายามผสานวิธีเชิงรูปนัยเข้ากับเอเจนต์
- Jane Street สามารถ ควบคุมภาษา ที่ใช้อยู่ได้อย่างลึกซึ้ง จึงสามารถปรับภาษาให้เหมาะกับแนวทางที่เน้นการพิสูจน์มากขึ้นได้
- มีหลายทิศทางที่เป็นไปได้
- สามารถผสานสเปกของคุณสมบัติแบบโมดูลาร์เข้ากับระบบชนิดข้อมูลได้
- สามารถเพิ่มข้อจำกัดระดับชนิดข้อมูลสำหรับองค์ประกอบอย่าง ownership และ mutability เพื่อให้บทพิสูจน์บางแบบง่ายขึ้น
- สามารถใส่เทคนิคการพิสูจน์เข้าไปในภาษาได้โดยตรง
-
ชุมชนนักพัฒนาที่พร้อม
- ที่ Jane Street มี ชุมชนนักพัฒนา ที่พร้อมจะรับแนวทางเหล่านี้
- สำหรับคนที่ทำงานด้านภาษาโปรแกรม เรื่องที่ยากกว่าการคิดไอเดียการเขียนโปรแกรมที่ดีกว่า คือการทำให้คนเอาไอเดียนั้นไปใช้ในงานจริง
- ที่ Jane Street มักมีผู้ใช้บ่นอยู่เสมอว่า ฟีเจอร์ใหม่ของระบบชนิดข้อมูลที่สัญญาไว้และยังไม่คุ้นเคยนั้นออกมาไม่เร็วพอ
- มีคนจำนวนมากที่มีพื้นฐานพร้อมใช้เทคนิคเหล่านี้ และความสนใจในการสร้างผลลัพธ์ที่ถูกต้องกับซอฟต์แวร์คุณภาพสูงก็หยั่งรากอยู่แล้ว
- ฐานผู้ใช้ที่กระตือรือร้นและมีความคาดหวังสูงทำให้มีอิสระที่จะลองทั้งการปรับปรุงระยะสั้นและวิสัยทัศน์ระยะยาวไปพร้อมกัน
- การปรับปรุงระยะสั้นสามารถสร้างผลกระทบได้ค่อนข้างเร็ว
- ส่วนวิสัยทัศน์ระยะยาวคือเป้าหมายที่ทะเยอทะยานกว่าซึ่งอาจใช้เวลาหลายปีกว่าจะไปถึง
- เราสามารถเรียนรู้จากความพยายามระยะสั้นไปพร้อมกับสร้างไปสู่เป้าหมายระยะยาว
-
ความสัมพันธ์กับเครื่องมือภายนอก
- พวกเขาไม่ได้มองข้ามงานจากโลกภายนอก และได้รับทั้งความคาดหวังและแรงบันดาลใจจากงานในชุมชนภาษาโปรแกรมหลายแห่ง
- เครื่องมือที่เกี่ยวข้องมีทั้ง Lean, Dafny, Rocq, Agda, Iris
- พวกเขากำลังมองหาวิธีผสาน OxCaml เข้ากับเครื่องมือบางตัว เพื่อใช้ประโยชน์จากโครงสร้างพื้นฐานชั้นยอดที่มีอยู่แล้ว
- และยังมองว่ามี ข้อได้เปรียบเฉพาะตัว ที่จะทำให้เกิดขึ้นได้ก็ต่อเมื่อจัดการทั้งภาษาและเทคนิคการพิสูจน์ไปพร้อมกัน
การเข้าร่วมทีม
- Jane Street กำลังมองหาบุคลากรด้านวิธีเชิงรูปนัยใน London และ New York
- ตอนนี้การสัมภาษณ์และการสร้างทีมสำหรับตำแหน่งนี้ยังอยู่ในช่วงเริ่มต้น
- ยังมีงานอีกมากที่ต้องทำ และพวกเขากำลังมองหาคนที่จะมาร่วมทีม
เพิ่มเติม
- โมเดลยังคงต้องการความช่วยเหลือและการชี้นำจากมนุษย์เมื่อต้องรับมือกับบทพิสูจน์ที่ซับซ้อน
- โปรแกรมเมอร์มนุษย์อาจมีไอเดียว่าเหตุใดระบบจึงทำงาน และควรพิสูจน์มันอย่างไรในระดับสูง
- โปรแกรมเมอร์ส่วนใหญ่ไม่รู้วิธีเข้ารหัสแนวคิดของบทพิสูจน์ให้อยู่ในรูปแบบที่สอดคล้องกับระบบพิสูจน์เฉพาะตัว
- โมเดลสามารถทำงานซ้ำ ๆ จำนวนมากให้เป็นอัตโนมัติ และมอบความเชี่ยวชาญในรายละเอียดเชิงเทคนิคของการเขียนบทพิสูจน์ได้
- ช่องทางหลบเลี่ยงอย่าง
Obj.magicอาจทำให้สามารถข้ามข้อจำกัดระดับชนิดข้อมูลได้ - หากติดตามและห้ามข้อยกเว้นแบบนี้ในโค้ดส่วนใหญ่ ก็จะเข้าใกล้สถานะของการรับประกันแบบครอบจักรวาลได้มาก
- วิธีเชิงรูปนัยสามารถทำให้เหตุผลว่าทำไมการใช้ช่องทางหลบเลี่ยงเหล่านี้จึงปลอดภัย กลายเป็นสิ่งที่ระบุไว้อย่างชัดเจน
1 ความคิดเห็น
ความคิดเห็นจาก Hacker News
เมื่อหลายสิบปีก่อนเคยทำงานด้าน การพิสูจน์ความถูกต้อง และในตอนนั้นระบบดังกล่าวมีการทำงานอัตโนมัติในการพิสูจน์มากกว่าหลายระบบที่มาทีหลังเสียอีก
ส่วนที่ง่ายนั้นให้ตัวทำให้เรียบแบบ Oppen-Nelson ซึ่งเป็น SAT solver ตัวแรกจัดการ ส่วนที่ยากนั้นเป็นหน้าที่ของตัวพิสูจน์ Boyer-Moore ที่ใช้ฮิวริสติกและบทตั้งช่วยที่มีอยู่ก่อนแล้ว งานยากของมนุษย์คือให้ตัวพิสูจน์ลองทำก่อน แล้วค่อยเสนอ บทตั้งช่วย ที่จะใช้กับการพิสูจน์ในภายหลัง
หลังจากนั้นดูเหมือนว่าระบบต่าง ๆ จะมีระบบอัตโนมัติน้อยลง และมองว่าสาเหตุที่ formal methods หลงทางก็เพราะหมกมุ่นกับรูปแบบนิยมมากเกินไปจนห่างจากงานจริง จากมุมมองของคนที่ต้องการโค้ดไร้บั๊กในโปรเจกต์เชิงพาณิชย์ รู้สึกว่าโปรเจกต์แบบวิชาการติดอคติแบบนักคณิตศาสตร์ที่ชอบสัญกรณ์สั้น ๆ สำหรับลงบทความและการวิเคราะห์กรณีให้น้อยที่สุด
ในความเป็นจริงจำเป็นต้องมีงานอัตโนมัติที่ไล่ทำอย่างหนักจำนวนมาก และต้องใช้ความหยั่งรู้น้อยลง คนฉลาดพยายามหลีกเลี่ยงความเยิ่นเย้อของการพิสูจน์ด้วยกระดาษและดินสอ จึงสร้างตรรกะแบบใหม่อย่าง modal logic และ temporal logic ขึ้นมาเรื่อย ๆ แต่ก็ไม่ได้ช่วยมากนัก ความจริงพื้นฐานของวงการนี้คือทฤษฎีบทส่วนใหญ่นั้นค่อนข้างธรรมดา
อย่างที่คนของ Jane Street พูดไว้ ความสามารถในการควบคุมภาษา เป็นข้อได้เปรียบใหญ่ ประโยคสำหรับการตรวจพิสูจน์ควรถูกรวมอยู่ในภาษาโปรแกรม และถ้ามันไปอยู่ในคอมเมนต์ ไวยากรณ์อีกชุด หรือไฟล์แยก ก็จะเพิ่มงานที่ไม่จำเป็น ดูแล้วการที่ Jane Street ผลักดันไปในทิศทางนี้เป็นเรื่องดี
ทำเรื่องนี้เร็วเกินไปตั้งแต่เมื่อกว่า 40 ปีก่อน ตอนนั้นการสร้างทฤษฎีจำนวนขึ้นมาใหม่ตั้งแต่ต้นด้วยตัวพิสูจน์ Boyer-Moore ใช้เวลาคำนวณราว 45 นาที แต่ตอนนี้ใช้ไม่ถึง 1 วินาที
https://archive.org/details/manualzilla-id-5928072/page/n3/m...
ตรรกะมีสถานะในวิทยาการคอมพิวเตอร์และวิศวกรรมซอฟต์แวร์คล้ายกับแคลคูลัสในฟิสิกส์ วิศวกรรมเครื่องกล และวิศวกรรมโยธา อย่าง LTL หรือ separation logic ในช่วงหลังถือเป็นความก้าวหน้าครั้งใหญ่
ความนิยมพอสมควรของ TLA+ ก็เป็นหลักฐานของเรื่องนั้น และ model checking ก็ใช้งานได้จริงมาก ประเด็นน่าตื่นเต้นตอนนี้คือ formal methods ที่หนักกว่านี้ โดยเฉพาะการพิสูจน์ทฤษฎีบท อาจมีต้นทุนต่ำพอที่จะใช้กับซอฟต์แวร์ระบบทั่วไปได้ด้วย
การเขียนข้อกำหนดเชิงรูปแบบสำหรับฟังก์ชัน แล้วสังเคราะห์มันด้วยไฮบริดของ SAT/SMT, ตัวพิสูจน์ทฤษฎีบท และ LLM พร้อมพิสูจน์ความถูกต้อง อาจกลายเป็นมาตรฐานในอีกไม่นานก็ได้
On the Unusual Effectiveness of Logic in Computer Science: https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf
From Philosophical to Industrial Logics: https://www.cs.rice.edu/~vardi/papers/icla09.pdf
สิ่งที่น่ากังวลคืออาจเกิดคณิตศาสตร์ที่ถอดความได้ยากขึ้นมา แล้วมีคนกลุ่มเล็ก ๆ ที่ศรัทธาในมันคอยเฝ้าดูแล สัญกรณ์ยาก ๆ ที่แตกต่างกันเหล่านั้นเข้ากันไม่ได้ และถึงจะเข้าใจอันหนึ่งก็อาจแทบไม่ช่วยให้เข้าใจอีกอันเลย คนส่วนใหญ่สุดท้ายอาจเขียนได้แค่ประโยคภาษาอังกฤษที่ตรวจพิสูจน์อย่างแท้จริงไม่ได้
ที่แย่กว่านั้นคืออาจปล่อยให้เครื่อง formalize ประโยคของตัวเอง แล้วเข้าร่วม ละครแห่งการตรวจพิสูจน์ ทั้งที่ไม่เข้าใจทั้งรูปแบบนิยมหรือการพิสูจน์นั้นเลย ก่อนจะทำเป็นตกใจเมื่อทุกอย่างพังลงมา
ตอนนี้มีความพยายามค่อย ๆ รวมความสามารถแบบนี้เข้าไปในส่วนที่ระบบชนิดจัดการได้ไม่เร็วพอ จึงสนใจมุมมองจากคนที่เคยเดินเส้นทางนี้มาก่อน
ดีมาก ช่วงไม่กี่เดือนมานี้ได้ย้ายไปใช้ ชนิดข้อมูลที่แสดงออกได้สูง ใน Scala 3 เพื่อให้ชนิดข้อมูลเก็บการพิสูจน์ตอนคอมไพล์ได้มากขึ้นเรื่อย ๆ ไม่ได้ใช้แมโคร แต่มีบางตัวที่ก็น่าใช้
วิธีนี้ไม่ได้แค่ช่วยลดปัญหาที่การทดสอบแบบเอเจนต์แพร่กระจายไปทั่วเท่านั้น แต่ดูเหมือนยังช่วยกันไม่ให้เอเจนต์ถอยไปใช้รูปแบบการทำงานคุณภาพต่ำด้วย โดยเฉพาะช่วยหยุด การสะสมคำนาม ที่เอเจนต์พยายามสร้าง singleton type ใหม่สำหรับทุกอย่าง แม้ในกรณีที่ควรสรุปทั่วไปอย่างมีเหตุผล
มองว่าด้านที่จะเร่งการเขียนโค้ดด้วยเอเจนต์คุณภาพดีได้ คือเครื่องมือที่คล้าย formal methods รวมถึงภาษาแบบที่มีระบบชนิดแข็งแรง
ในที่นี้ ชนิดข้อมูลที่แสดงออกได้สูง หมายถึงเทคนิคที่ถ้าทีมยังไม่คุ้นกับการเขียนโปรแกรมระดับชนิดข้อมูลอยู่แล้ว ก็คงไม่อยากใส่เข้าไปในโค้ดเบสทั่วไป กล่าวคือควรเป็นทีมที่มอง higher-kinded types และ type functions ไม่ใช่ของประหลาด แต่เป็นบล็อกพื้นฐาน
เอเจนต์นั้นในแง่ความรู้มัก “เก่งคณิต” กว่านักพัฒนาส่วนใหญ่ และหลายครั้งยังดีกว่านักพัฒนาที่หมกมุ่นกับ category theory เสียอีก ยิ่งถ้ามองว่ามันมีความอดทนกับบทสนทนาแบบ “ไร้ขีดจำกัด” ก็ยิ่งสอนได้ดีพอสมควร
ส่วนตัวเคยให้ Codex แปลงงานพิสูจน์เล่น ๆ บางชิ้นไปเป็นสไตล์ Lean ซึ่งง่ายมาก ไม่ถึงกับจะบอกว่า “ถูกต้อง” 100% และถ้าจะตรวจให้ละเอียดกว่านี้ก็คงต้องเรียน Lean 4 เพิ่ม แต่โดยพื้นฐานแล้วมันดูเหมือนตรวจจุดพลาดแบบคลาสสิกของการพิสูจน์ได้ด้วย อนาคตของ formal methods น่าตื่นเต้นมาก
ดูเหมือนว่าแนวคิดคือ เมื่อ Gen AI สร้างโค้ดจำนวนมากขึ้น ก็ควรย้ายคุณค่าของมนุษย์ไปอยู่ที่ฝั่งของการตรวจสอบยืนยัน เลยทำให้ผมกลับมาคิดเป็นครั้งคราวว่าแท้จริงแล้วการเขียนโปรแกรมคืออะไรกันแน่
สำหรับคนที่ไม่ได้ใช้ภาษาอังกฤษเป็นภาษาแม่ การเรียนเขียนโปรแกรมเองก็เป็นความท้าทายใหญ่พออยู่แล้ว
ถ้าจะทำความเข้าใจเอกสารภาษาอังกฤษที่ยังไม่ได้แปล ก็ต้องพึ่งการแปลด้วยเครื่อง และสื่อการสอนในภาษาของผมเองก็มักตามหลังอยู่ราว 5~6 ปี
ตอนนี้การรีวิวโค้ดหลายหมื่นบรรทัดที่ AI สร้างขึ้นมาแทบเป็นไปไม่ได้ จึงเริ่มเห็นการพูดถึงการตั้งกฎแบบสัมบูรณ์คล้ายการพิสูจน์ทางคณิตศาสตร์ พออ่านบทความนี้แล้วผมนึกถึง borrow checker ของ Rust ขึ้นมาทันที และพอได้ใช้ Rust จริง ๆ สักสองสามครั้ง ก็มักเห็นว่าคนพยายามหาทางเลี่ยง borrow checker จนกลายเป็นนิสัยไม่ดี
ถ้าความเข้มงวดทางคณิตศาสตร์มากเกินไป มนุษย์ก็มักจะหาทางอ้อม โดยเฉพาะโปรแกรมเมอร์ที่พื้นฐานการศึกษาไม่มากอย่างผมยิ่งเป็นแบบนั้นได้ง่าย
สุดท้ายความพยายามแบบนี้อาจนำไปสู่การเขียนโค้ดที่รองรับได้แค่คำตอบแบบทำให้เป็นรูปแบบตายตัวบางชนิดเท่านั้น ถ้ามันถูกทำให้เป็นมาตรฐานแบบนั้น ผมก็ยังไม่แน่ใจว่าจะตอบสนองความต้องการของมนุษย์ได้จริงหรือไม่
ความพยายามแบบ defensive programming นี้ก็โอเคอยู่ แต่ถ้าใช้คำที่ผมตั้งเอง ผมอยากทำ aggressive programming มากกว่า คือยอมรับความเสี่ยง แต่แก้ให้ไว ส่งขึ้นระบบให้ไว และเชื่อว่าเมื่อเวลาผ่านไปมันจะดีพอเอง
แน่นอนว่าในอุตสาหกรรมเดิมอย่าง Jane Street ที่ความถูกต้องแม่นยำสำคัญมากและขอบเขตงานถูกนิยามไว้ชัดเจน แนวทางในบทความนี้เหมาะสม เพราะมีข้อมูลมากพอที่จะจำลองความต้องการของตลาดได้อย่างเหมาะสม
แต่สำหรับคนอย่างผมที่ต้องคอยย้ายที่ไปเรื่อย ๆ เพื่อหาเหมืองทองไว้ทำเงิน วิธีแบบนี้ดูเป็นความฟุ่มเฟือยสำหรับผู้แพ้ทางสังคมอยู่เหมือนกัน ธุรกิจเดิมที่มีการสร้างแบบจำลองอย่าง成熟ต้องอาศัยบุคลากรผู้เชี่ยวชาญการศึกษาสูงคอยปรับให้เหมาะสมต่อเนื่อง ซึ่งผมก็รู้อยู่แล้วว่าในโลกจริง ความต้องการแบบนั้นตามไม่ทันแน่ ๆ เลยพยายามหาพื้นที่ที่การทำโมเดลยังไม่เป็นระบบ แต่ก็ยังไม่แน่ใจว่าแนวทางนี้จะใช้ได้แม้ในที่แบบนั้นหรือเปล่า
ที่นั่นไม่มีคำว่า “ค่อยแก้ทีหลังได้”
เพราะกว่าคุณจะเข้าใจว่าอะไรผิดพลาด ก็อาจเสียเงินไปหลายพันล้านแล้ว
เพราะงั้นแนวทางแบบ aggressive อาจใช้ได้ในส่วนที่ไม่ใช่แกนหลัก
อนึ่ง ทุกวันนี้เราก็ใช้แนวทาง defensive กันอยู่แล้วในหลายจุด Python, Java ฯลฯ มีกลไก garbage collector และนั่นก็เท่ากับมีการยืนยันว่าโค้ดจะทำงานตามเจตนาในระดับหนึ่ง
ผมสงสัยมาสักพักแล้วว่า formal verification จะเริ่มโผล่มาเมื่อไร และการขยับจากขั้นที่กังวลเรื่องรายละเอียดการ implementation ไปสู่ขั้นที่อธิบายปัญหาในเชิงวิทยาศาสตร์และคณิตศาสตร์ก็ดูเป็นธรรมชาติดี
เพราะ Gen AI ต้นทุนของ defensive programming ลดลงมาก ขณะที่ต้นทุนของการตรวจสอบโดยมนุษย์เพิ่มขึ้นมาก ในทางกลับกัน formal methods ทำให้การตรวจสอบถูกลง แต่มี overhead ฝั่ง implementation สูง ทั้งจากการต้องเขียนสเปก, type, proof และต้องดัด implementation ให้เข้าโครงที่แข็งแรง
แต่ตอนนี้ Gen AI อาจทำงานยากพวกนั้นให้เป็นอัตโนมัติได้ ทั้งสองอย่างจึงเข้ากันอย่างยิ่ง
มันอาจต้องออกแรงบ้างเล็กน้อย แต่การตัด overhead จากการแปลที่ต้องเกิดซ้ำ ๆ ออกไปได้จะช่วยอย่างมหาศาล
เพียงแต่ผมไม่ค่อยเข้าใจว่าการเรียกตัวเองว่า “ผู้แพ้ทางสังคม” หรือการที่คุณไม่ได้ทำตามแนวปฏิบัตินี้ในเส้นทางอาชีพของตัวเอง มันเกี่ยวข้องกับประเด็นนี้อย่างไร
ช่วงนี้ผมกำลังลองเล่นกับแนวคิดที่เกี่ยวข้องกันอยู่ และสิ่งที่น่าประหลาดใจก็คือ โมเดลแนวหน้า โดยเฉพาะ ChatGPT-5.5 สามารถช่วยทำ proof แบบ manual เฉพาะจุดใน Roqc ซึ่งคือ proof assistant Coq เดิม ได้ดีแค่ไหน
proof อาจไม่ได้สวยเสมอไป แต่ ChatGPT มักพิสูจน์สิ่งที่สำหรับผมซึ่งมีประสบการณ์กับ proof assistant อยู่บ้างแม้จำกัด และมีประสบการณ์โดเมนในด้าน lemma ที่กำลังพิสูจน์อยู่พอสมควร จะต้องใช้เวลานานกว่ามาก ให้เสร็จได้ภายในไม่กี่นาทีและในรอบลอง 10~100 ครั้ง
สิ่งที่น่าสนใจในบริบทของโพสต์สั้น ๆ นี้คือ มันไปสั่นคลอนสมมติฐานพื้นฐานที่ทำให้เครื่องมือ formal methods บางตัวทำงานอยู่ได้ Frama-C, Ada/SPARK และอื่น ๆ เน้นการสร้าง proof obligation ที่เครื่องมืออย่าง CVC5, Z3 สามารถจัดการอัตโนมัติได้ และถ้าล้มเหลวก็ต้องถอยไปใช้ทางเลือกที่ค่อนข้างทรมานคือทำ proof แบบ manual ใน Roqc
ขั้นตอนที่พบบ่อยคือเจอว่า obligation บางอัน “ยาก” เกินไป คือแก้อัตโนมัติไม่ได้ แล้วจึงกลับไปจัดชุด lemma และ assertion ที่มองเห็นได้จากจุดในโค้ดที่สร้าง obligation นั้นใหม่เพื่อทำให้มัน “ง่าย” ขึ้น หรือไม่ก็กระทั่งแก้โค้ดเอง
มันสมเหตุสมผลในโลกที่ proof ใน Roqc มีต้นทุนแพงเป็นสองเท่า เพราะมนุษย์เขียนยาก และเมื่อโค้ดกับ proof รอบข้างเปลี่ยน ค่าแปรผันของการบำรุงรักษาก็สูง
แต่ถ้า proof ใน Roqc กลายเป็น “การแก้อัตโนมัติโดยมี AI อยู่ในลูป” ความต่างด้านต้นทุนนี้ก็จะหายไป แบบนั้นเราก็อาจเขียน proof ได้เหมือนเขียนโค้ด โดยให้ความชัดเจนที่มนุษย์อ่านง่ายเป็นลำดับแรก และค่อยสนใจการปรับให้เหมาะกับ compiler หรือ prover ทีหลังมาก ๆ ผมยังย่อยผลกระทบทั้งหมดของเรื่องนี้ไม่หมด แต่คิดว่ามันน่าสนใจมาก
ผมไม่เคยทำงานกับ proof มาก่อน แต่เคยเห็นบ่อยเหมือนกันว่าเมื่อบอก AI ว่า “หลังเปลี่ยนแล้ว test นี้ fail” มันไม่ได้แก้โค้ดให้ผ่านทั้ง test เดิมที่ผมตั้งใจไว้และ test ใหม่ แต่กลับไปแก้ตัว test เองแทน
อนาคตดูน่าตื่นเต้นดี
ทุกครั้งที่อ่านเรื่อง formal specification มันดูเหมือนเป็น “การเขียนเทสต์เดิมในอีกรูปแบบหนึ่ง” และที่แย่กว่านั้นคือดูเหมือนเป็น “การเขียน implementation เดิมในอีกรูปแบบหนึ่ง”
การเขียนซ้ำสองรอบอาจช่วยจับข้อผิดพลาดได้ก็จริง แต่ถ้า formal specification เองก็มีบั๊กแบบเดียวกับเทสต์หรือ implementation ได้ ผมก็ไม่ค่อยเข้าใจว่าอะไรคือจุดที่พิเศษ
ปัญหาพื้นฐานคือ ถ้าจะพิสูจน์อย่างเป็นทางการว่าโปรแกรมทำ “บางอย่าง” ได้ เราก็ต้องนิยาม “บางอย่าง” นั้นให้เฉพาะเจาะจงมาก ๆ ซึ่งสุดท้ายมันก็แทบจะกลายเป็นการเขียนเทสต์หรือ implementation ใหม่อีกครั้ง
ผมตามดูหัวข้อนี้เป็นพัก ๆ มาหลายปีแล้ว และยังรู้สึกตลอดว่าตัวเองคงพลาดอะไรบางอย่างอยู่ แต่ก็ไม่รู้ว่าคืออะไร ใครช่วยอธิบายได้ไหม
ข้อบกพร่องของการทดสอบคือเราทดสอบได้เฉพาะพฤติกรรมที่เราคิดได้ว่ามันอาจเป็นปัญหาเท่านั้น ถ้าอยากแก้พฤติกรรมที่เราไม่รู้มาก่อนด้วยว่ามันอาจพังได้ ก็ต้องใช้เครื่องมือที่พิเศษกว่านั้นในชุดเครื่องมือของเรา fuzz testing เป็นจุดเริ่มต้นหนึ่งในทิศทางนั้น และ formal verification ก็เป็นอีกจุดเริ่มต้นหนึ่ง
แน่นอนว่าคุณภาพของเครื่องมือเหล่านี้ขึ้นอยู่กับว่าเราจะเขียน formal model ที่ครอบคลุม ซึ่งอนุญาตพฤติกรรมที่ต้องการและห้ามพฤติกรรมที่ไม่ต้องการ ได้ดีแค่ไหน และในหลายสาขาเราก็ยังห่างจากจุดนั้นอย่างน่าประหลาดใจอยู่มาก
ตัวอย่างเช่น ใน unit test เราอาจเขียนว่า “foo('abc') คืนค่าเป็นสตริงที่ไม่มีช่องว่างท้าย”
แต่ด้วย formal methods เราสามารถพิสูจน์ได้ว่า “สำหรับอินพุตใด ๆ x, foo(x) จะคืนค่าเป็นสตริงที่ไม่มีช่องว่างท้าย”
นี่เป็นตัวอย่างง่าย ๆ แต่ก็พอนึกถึงสิ่งที่ซับซ้อนกว่านี้ได้ เช่น “สำหรับโปรแกรมใด ๆ P, compile(P) จะมีพฤติกรรมเหมือนกับ P”
แน่นอนว่าเราต้องนิยามก่อนว่า “มีพฤติกรรมเหมือนกัน” หมายถึงอะไร
คุณระบุคุณสมบัติของแบบออกแบบ แล้วเครื่องมือจะทดสอบแบบออกแบบในหลาย ๆ วิธีเพื่อดูว่าสามารถละเมิดคุณสมบัตินั้นได้หรือไม่
ตัวอย่างเช่น ถ้าเป็นระบบควบคุมสัญญาณไฟจราจร คุณสามารถระบุคุณสมบัติได้ว่า เลนที่ตัดกันจะไม่สามารถเป็นไฟเขียวพร้อมกัน หรือกลายเป็นไฟเขียวทั้งคู่ภายในช่วงเวลาหนึ่งได้
เครื่องมือจะตรวจสิ่งนี้ด้วย การสำรวจครบทุกกรณี และสามารถแสดง trace ของโค้ดที่ทำให้เกิดการละเมิดได้
type system ที่พิสูจน์ได้แบบ static ช่วยให้แต่ละองค์ประกอบถูกตรวจล่วงหน้าว่าเข้ากับองค์ประกอบอื่นทั้งหมดได้ ไม่ใช่แค่ “เทสต์นี้ผ่าน” แต่รับประกันได้ว่าเมื่อประกอบเข้าด้วยกันแล้ว “เทสต์ทั้งหมดนี้สร้างภาพรวมที่สมเหตุสมผลและสอดคล้องกัน” และป้องกันไม่ให้ model ที่ไม่สอดคล้องกันถูกนำไป implement ในโค้ด
มันคล้ายกับการขยายแนวคิดของ
matchใน Rust ที่บังคับให้ครอบคลุมทุกแขนงที่เป็นไปได้ ออกไปในระดับทั้ง codebaseก็จริงที่มันจับความผิดพลาดด้านตรรกะพื้นฐานหรือความผิดพลาดเชิงทฤษฎีไม่ได้ แต่คุณอาจประหลาดใจว่ามันแข็งแกร่งกว่าการเอา Haskell type system, การทดสอบเชิงฟังก์ชันแบบเฉพาะกิจ, และ property testing มารวมกันมากแค่ไหน แม้ทั้งหมดนั้นโดยรวมก็ถือว่าเป็นระบบที่แข็งแรงอยู่แล้ว แต่คริปโตกราฟีที่พิสูจน์อย่างเป็นทางการนั้นมีมาตรฐานสูงกว่านั้นมาก
สิ่งนี้มีคุณค่าเป็นพิเศษในสถานการณ์ concurrent, distributed, และ multi-thread เพราะ race condition กับ deadlock นั้นทั้งทดสอบและให้เหตุผลได้ยากมาก ปัญหาอย่าง “A, B, C สามารถเกิดในลำดับ A, C, B ได้หรือไม่” ก็เป็นตัวอย่างหนึ่ง
ความก้าวหน้าของสาขานี้น่าจะไปประมาณนี้ อย่างแรก LLM จะทำให้การเรียนรู้และการใช้งาน formal methods เร็วขึ้นมาก แม้ในช่วงแรกมันอาจยังเป็นเพียงการตรวจย้อนหลังแบบ “ลองรอบที่สอง”
อย่างที่สอง มันจะขยับไปสู่ระบบอัตโนมัติที่ให้ LLM ช่วยตรวจว่า “โค้ด implementation เปลี่ยนไปแล้ว ดูเหมือนว่ามันทำให้ model พังหรือเปล่า?” แม้มันจะยังไม่เด็ดขาด แต่ก็น่าจะดีกว่าการให้คนต้องรีวิวอะไรบางอย่างที่เปลี่ยนไม่บ่อยมากอยู่มาก
อย่างที่สาม การก้าวกระโดดจริง ๆ น่าจะอยู่ที่การยกระดับเครื่องมือประเภท “เขียนแค่ formal specification แล้วให้สร้าง implementation ออกมา” ไปอีกขั้น มีโปรเจ็กต์สร้างโค้ดแบบนี้อยู่หลายตัวแล้ว แต่ส่วนใหญ่ยังไม่สุกงอมพอถึงระดับที่บริษัทต่าง ๆ ต้องการ จะเป็นอย่างไรถ้าเครื่องมือ LLM ช่วยเร่งงานปรับแต่งหนึ่งในนั้น ซึ่งปกติต้องใช้แรงคน 1-2 ปี ให้เร็วขึ้นได้
บทความก่อนหน้าของ Kleppmann https://martin.kleppmann.com/2025/12/08/ai-formal-verificati... ก็น่าอ่านเช่นกัน และอะไรที่สามารถใส่เข้าไปใน type system หรือ linter ได้ ก็ควรชั่งน้ำหนักว่าจะทำแบบนั้นแน่นอน
หวังว่าจะมีวิธีที่ใช้งานสะดวกกว่านี้ จากเครื่องมือที่กล่าวถึงในบทความ ดูเหมือนว่า dafny กับ iris จะใกล้เคียงงานอุตสาหกรรมมากที่สุด เท่าที่ผมทราบ Amazon S3 ก็มีประวัติการใช้ TLA ภายในด้วย
แต่ผมยังไม่เคยเห็น สิ่งที่เทียบได้กับ TypeScript สำหรับวงการนี้ อะไรบางอย่างที่เข้าไปอยู่กับเครื่องมือเดิมได้อย่างเป็นธรรมชาติ ทำงานเหมือน zero-cost abstraction และทำให้คนชอบมันจากใจมากกว่าวิธีเดิม
การใช้ custom linter เองก็ยังค่อนข้างแย่อยู่ดี golangci-lint เป็น codebase ที่ทรมาน ส่วน semgrep ผมยังไม่เคยใช้ แต่ rule engine ของมันดูน่ากดดัน และผมก็ยังไม่เคยใช้ AST API ที่ถูกใจเลย
คำสรรเสริญต่อการให้เหตุผลแบบนิรนัย หรือก็คือ “formal methods” ในลักษณะนี้ มักละเลยข้อจำกัดพื้นฐานของมันเสมอ นั่นคือปัญหาว่า สัจพจน์และคำนิยามสอดคล้องกับโดเมนเป้าหมายได้ดีแค่ไหน
มันก็เหมือนคำพูดที่ว่า “ในทางทฤษฎี ทฤษฎีกับการปฏิบัติไม่ต่างกัน แต่ในทางปฏิบัติ…” Jane Street น่าจะคาดว่าพวกเขาจะดูแลโค้ดเบสขนาดใหญ่ที่มีการจับคู่แบบ 1:1 เพราะเป้าหมายของโค้ดคือการทำอัลกอริทึมเชิงกำหนดให้เป็นจริง นักพัฒนาจำนวนมากทำงานในโดเมนแบบนั้น แต่คนนับล้านไม่ได้เป็นเช่นนั้น โดยเฉพาะ UI ส่วนใหญ่ และงานเชิงสำรวจส่วนใหญ่ก็เป็นแบบนั้น
ควบคู่ไปกับ formal methods ก็ยังมีแนวทางที่พยายามนิยามเกณฑ์การยอมรับให้ละเอียดมากขึ้น แม้จะไม่ใช่แนวทางเชิงตรรกะหรือคณิตศาสตร์ แนวทางนี้อย่างน้อยก็ต้องต่อสู้กับปัญหาเรื่องการแมป แต่ก็ยังแก้ไม่ได้ในสถานการณ์ส่วนใหญ่ที่แผนที่ไม่ใช่อาณาเขตจริง
หน้าผลการค้นหาของ Google มีเฟรมเวิร์กการปรับให้เหมาะสมภายในที่พัฒนาไปไกลมาก แต่ได้ไปถึงจุดที่ดีที่สุดจริงหรือยัง? หรือพร็อตไทป์ที่ทำขึ้นอย่างเร่งรีบเพื่อจับไอเดียที่ยังพร่าเลือนอาจแสดงให้เห็นได้ดีกว่ากัน? คำถามแบบนี้ตอบได้ดีที่สุดเมื่อมองออกไปยังสิ่งภายนอกที่ระบบนั้นรับใช้ ไม่ใช่มองแค่ภายในตัวระบบเอง
วงจรตรรกะ องค์ประกอบ CPU ที่ใช้ formal verification อย่างหนัก เคอร์เนล โปรโตคอล พาร์เซอร์ คอมไพเลอร์ วิทยาการเข้ารหัส เฟรมเวิร์กความปลอดภัย และ primitive ด้าน concurrency ต่างได้ประโยชน์จากการพิสูจน์ความถูกต้องอย่างมาก
ถ้าอยากศึกษาเพิ่มเติม บทความของ Hillel Wayne เป็นจุดเริ่มต้นที่ดี: https://www.hillelwayne.com/formally-specifying-uis/
และในบางกรณี เราอาจเรียนรู้ได้แม้ผลลัพธ์จะไม่ได้ถูกนิยามไว้อย่างชัดเจน ดังนั้นมันไม่ได้เป็นเพียงปัญหาที่ต้องนั่งคิดว่าควรมีความหมายอย่างไรเท่านั้น
ในฐานะคนที่สนใจการออกแบบและการอิมพลีเมนต์ภาษาโปรแกรมอยู่บ้าง ประโยคนี้น่าสนใจมากจริง ๆ: “สำหรับคนส่วนใหญ่ที่ทำงานกับภาษาโปรแกรม ส่วนที่ง่ายคือการคิดไอเดียใหม่ ๆ ที่ดีกว่าเพื่อทำให้การเขียนโปรแกรมดีขึ้น ส่วนที่ยากคือการโน้มน้าวให้ใครสักคนเอาไอเดียนั้นไปใช้กับงานจริง”
เห็นด้วยอย่างยิ่ง ถึงจะมีประโยชน์ แต่ก็มีขีดจำกัดของ ความแปลกใหม่ที่ยอมรับได้ ที่จะใส่ลงในภาษาใหม่
แต่ AI agent คงไม่ได้รู้สึกต่อต้านมากนักต่อไอเดียใหม่แบบสุดขั้วในการออกแบบภาษาโปรแกรม ฉันคิดมาสักพักแล้วว่าการออกแบบภาษาโปรแกรมจะพัฒนาไปอย่างไรหลังยุค agentic AI
เมื่อกังวลเรื่องการยอมรับใช้งานได้น้อยลงมาก การได้เห็นว่าเราจะสร้างไอเดียใหม่อะไรขึ้นมาเพื่อพัฒนาภาษาโปรแกรมได้บ้างก็น่าตื่นเต้นมาก
https://steveklabnik.com/writing/the-language-strangeness-bu...
ฉันกำลังทำงานในทิศทางของการนำ formal methods มาใช้กับฝั่ง application security testing และมองว่าวิธีเดียวกันนี้สามารถนำไปใช้กับการพิสูจน์ความถูกต้องของ business logic ได้ด้วย
เราใช้ taint analysis สำหรับเรื่องนี้ มันเป็นแนวทางของ formal methods ที่ค่อนข้างเป็นที่ยอมรับแล้ว แต่ในภาคสนามยังไม่ถูกใช้แพร่หลายมากนักเพราะความซับซ้อนของ data flow ในโค้ดเบสจริง
การขยาย formal methods ให้ไปไกลกว่าการจับคู่แพตเทิร์น AST และการตรวจชนิดแบบง่าย ๆ เป็นงานที่ยากมาก กว่าจะมาถึงระดับที่ใช้ taint analysis ไล่ตาม data flow ข้าม procedure ในโค้ดเบสจริงได้ภายในไม่กี่นาทีและค้นหาช่องโหว่ที่ซ่อนลึกได้ ต้องใช้เวลาวิจัยและพัฒนาหลายปี
ถ้าสนใจก็ดูโปรเจกต์ได้: https://github.com/seqra/opentaint
เมื่อประมาณ 18 เดือนก่อน ฉันเริ่มหมกมุ่นกับการใช้ types ร่วมกับ LLM และเริ่มจริงจังกับ
lean4เมื่อราว 6–8 เดือนก่อน ตอนนี้ฉันไม่คิดจะใช้ AI ช่วยงานซอฟต์แวร์เลย หากไม่มีพื้นฐานการพิสูจน์แบบCICที่มี C/C++ FFI ใช้งานได้จริง และจึงเชื่อมต่อกับแทบทุกอย่างได้เราแบนทุกอย่างตั้งแต่ JSON ไปจนถึง Python และยังเขียน
nixใหม่เพื่อให้มีคอมไพเลอร์ด้วย แทบทุกอย่างที่เราใช้นอกจากจะถูกทดสอบด้วย property testing และ fuzz testing หลายแบบจนถึงขีดสุดแล้ว อย่างน้อยยังมี proof ในlean4ที่ขับเคลื่อน property test ผ่านการเชื่อมต่อ.oleanอีกด้วย ถ้ามีเวลาเหลือ เราก็พิสูจน์ความครบถ้วนของทั้งโดเมนและทดสอบคุณสมบัตินั้นด้วยส่วนที่ต้องเร็วทั้งหมดถูกสร้างจาก
lean4ดังนั้นจึงข้ามการถกเถียง C++/Rust ไปได้ มีข้อดีตรงที่บั๊กใน C++ บางครั้งจริง ๆ แล้วคือบั๊กในโค้ดlean4แต่ก็ไปได้ทั้งสองทางมันเป็นการเปลี่ยนแปลงครั้งใหญ่ และฉันก็ไม่โทษคนที่สงสัยว่า “แบน JSON กับ Python เนี่ยนะ?” แต่เราได้ตรวจสอบโค้ดไปแล้วหลายล้านบรรทัดด้วยวิธีนี้ และ AI + formal system เป็นการก้าวกระโดดที่ใหญ่กว่าการเปลี่ยนจากไม่มี AI ไปเป็น AI กับ Python มาก อย่างหลังในประสบการณ์ของเรา ความก้าวหน้าไม่ได้เพิ่มขึ้นแบบสม่ำเสมอ แต่อย่างแรกนั้นแทบจะก้าวหน้าอย่างสม่ำเสมอเสมอ
ยังสามารถทำสิ่งที่ค่อนข้างกล้าหาญได้ด้วย นี่คือการพิสูจน์เชิงรูปแบบของการคำนวณ polyhedral tensor อย่างที่ ISL และ CuTe ทำการโมเดลไว้ และด้วยสิ่งนี้เราสามารถทำ swizzling และ tiling บนอุปกรณ์ด้วย
mdspanของ C++23 พร้อมทั้งพิสูจน์ได้ว่ามันถูกต้องด้วย เพียงแต่ตัวอย่างนี้ไม่ได้แสดงข้อโต้แย้งแบบ L'Hopital เกี่ยวกับ coverage ได้ดีนัก: https://github.com/b7r6/mdspan-cuteผลลัพธ์นั้นเร็วมาก และเร็วตั้งแต่ครั้งแรกที่ลอง
https://straylight.software/assets/lambda-hierarchy.svg