ภูมิทัศน์ของการตรวจสอบความถูกต้องอย่างเป็นทางการสำหรับภาษาโปรแกรมมิ่งยังคงพัฒนาต่อไป โดยมีเครื่องมืออย่าง coq-of-rust ที่มีเป้าหมายในการพิสูจน์ความถูกต้องของโค้ดในแอปพลิเคชัน Rust ด้วยคณิตศาสตร์ อย่างไรก็ตาม การสนทนาในชุมชนได้เผยให้เห็นถึงความละเอียดอ่อนที่สำคัญเกี่ยวกับสิ่งที่การตรวจสอบความถูกต้องอย่างเป็นทางการสามารถและไม่สามารถรับประกันได้ พร้อมกับข่าวการเปลี่ยนชื่อที่สำคัญในระบบนิเวศของการตรวจสอบ
ความเป็นจริงของการอ้างสิทธิ์การตรวจสอบความถูกต้องอย่างเป็นทางการ
ในขณะที่ coq-of-rust สัญญาว่าจะทำให้แอปพลิเคชันปราศจากข้อบกพร่องผ่านการพิสูจน์ทางคณิตศาสตร์ ชุมชนนักพัฒนาได้เน้นย้ำถึงความแตกต่างที่สำคัญ การตรวจสอบความถูกต้องอย่างเป็นทางการพิสูจน์ว่าโค้ดนั้นใช้งานข้อกำหนดได้อย่างถูกต้อง แต่ไม่สามารถรับประกันได้ว่าข้อกำหนดเองนั้นปราศจากข้อบกพร่อง
ผมชอบการตรวจสอบความถูกต้องอย่างเป็นทางการ แต่ผมคิดว่านี่เป็นการบิดเบือนสิ่งที่มันนำเสนอ มันช่วยให้คุณพิสูจน์ทางคณิตศาสตร์ว่าโค้ดของคุณใช้งานข้อกำหนดได้อย่างถูกต้อง มันไม่ได้พิสูจน์ว่าข้อกำหนดของคุณปราศจากข้อบกพร่องและช่องโหว่ มันไม่ได้พิสูจน์ว่าข้อกำหนดของคุณใช้งานกฎทางธุรกิจของคุณได้อย่างถูกต้อง
ความแตกต่างระหว่างการตรวจสอบ (โค้ดตรงกับข้อกำหนดหรือไม่?) และการตรวจสอบความถูกต้อง (ข้อกำหนดตรงกับความต้องการจริงหรือไม่?) เป็นแนวคิดพื้นฐานในการประกันคุณภาพ การตรวจสอบความถูกต้องอย่างเป็นทางการมีประสิทธิภาพในการพิสูจน์ว่าความไม่แปรผันยังคงอยู่สำหรับอินพุตทั้งหมดที่เป็นไปได้ ซึ่งมีคุณค่าเป็นพิเศษในกรณีที่ข้อกำหนดมีความซับซ้อนน้อยกว่าการใช้งาน เช่น ในฐานข้อมูลและระบบไฟล์
Coq กลายเป็น Rocq: การเปลี่ยนชื่อที่สำคัญ
การพัฒนาที่น่าสังเกตที่กล่าวถึงในความคิดเห็นคือ ผู้ช่วยการพิสูจน์ Coq ซึ่งเป็นพื้นฐานของ coq-of-rust ได้ถูกเปลี่ยนชื่อเป็น Rocq ตามการสนทนาในชุมชน การเปลี่ยนแปลงนี้เป็นผลมาจากการสำรวจชุมชนซึ่งประมาณ 24% ของผู้ใช้แสดงความไม่สบายใจกับชื่อเดิม โดยพบว่ามันทำให้รู้สึกไม่สบายใจหรือลำบากใจที่จะใช้ในสภาพแวดล้อมการทำงานแบบมืออาชีพ โครงการนี้ตอนนี้เป็นที่รู้จักอย่างเป็นทางการในชื่อ Rocq และสามารถพบได้ที่ rocq-prover.org
การเปลี่ยนชื่อได้จุดประกายปฏิกิริยาที่หลากหลาย โดยบางคนมองว่าเป็นวิวัฒนาการทางวิชาชีพที่จำเป็น ในขณะที่คนอื่นเสียใจกับการสูญเสียสิ่งที่พวกเขาถือว่าเป็นการเล่นคำที่ไม่มีพิษมีภัย
ตำแหน่งที่เป็นเอกลักษณ์ของ Rust ในการตรวจสอบ
โมเดลหน่วยความจำแบบ mutable-xor-aliased ของ Rust ทำให้มันเหมาะสมเป็นพิเศษสำหรับการตรวจสอบความถูกต้องอย่างเป็นทางการเมื่อเทียบกับภาษาอื่นๆ หลายภาษา โมเดลนี้ ซึ่งข้อมูลสามารถเป็นแบบ mutable หรือมีการอ้างอิงหลายครั้งได้แต่ไม่ใช่ทั้งสองอย่างพร้อมกัน สร้างพื้นฐานที่เครื่องมือตรวจสอบสามารถสร้างขึ้นได้อย่างมีประสิทธิภาพมากขึ้น
สมาชิกในชุมชนสังเกตว่าหากไม่มีโมเดลดังกล่าว การตรวจสอบจะยากพอๆ กัน — และไม่สามารถจัดการได้ในทางปฏิบัติพอๆ กับเครื่องมือตรวจสอบทั้งหมดสำหรับภาษาที่มีอยู่ สิ่งนี้ให้ความได้เปรียบที่อาจเกิดขึ้นในพื้นที่การตรวจสอบแก่เครื่องมือตรวจสอบที่ใช้ Rust เช่น coq-of-rust, Verus และอื่นๆ
เครื่องมือตรวจสอบความถูกต้องอย่างเป็นทางการสำหรับ Rust ที่กล่าวถึงในความคิดเห็น
- coq-of-rust: แปลง Rust เป็น Coq สำหรับการตรวจสอบความถูกต้องอย่างเป็นทางการ
- Verus: มุ่งเน้นการตรวจสอบระบบเต็มรูปแบบ (ระบบไฟล์ที่ได้รับการตรวจสอบ, ตัวควบคุม Kubernetes)
- Creusot: การแปลงจาก MIR ไปยัง Why3 (และต่อไปยังตัวแก้ปัญหา SMT)
- Ironclad/Gloire: ไม่เฉพาะเจาะจงสำหรับ Rust แต่เป็นเคอร์เนลระบบปฏิบัติการที่ได้รับการตรวจสอบอย่างเป็นทางการที่เขียนด้วย SPARK/Ada
ประเด็นสำคัญเกี่ยวกับการตรวจสอบความถูกต้องอย่างเป็นทางการ
- พิสูจน์ว่าโค้ดนำข้อกำหนดไปใช้อย่างถูกต้อง
- ไม่ได้พิสูจน์ว่าข้อกำหนดเองถูกต้อง
- มีประโยชน์อย่างยิ่งเมื่อข้อกำหนดง่ายกว่าการนำไปใช้
- ได้รับประโยชน์จากโมเดลหน่วยความจำ "mutable-xor-aliased" ของ Rust
แนวทางทางเลือกและคู่แข่ง
ภูมิทัศน์ของการตรวจสอบความถูกต้องอย่างเป็นทางการขยายไปไกลกว่า coq-of-rust สมาชิกในชุมชนได้เน้นย้ำถึงทางเลือกหลายอย่าง รวมถึง Verus สำหรับการตรวจสอบระบบ (ใช้ในระบบไฟล์ที่ได้รับการตรวจสอบและตัวควบคุม Kubernetes) และเคอร์เนล Ironclad กับ Gloire OS ที่สร้างขึ้นบนมันโดยใช้ SPARK และ Ada
นักพัฒนาบางคนแสดงความสนใจที่จะเห็นแนวทางการตรวจสอบที่คล้ายกันนำไปใช้กับภาษาอื่นๆ เช่น Zig โดยเฉพาะอย่างยิ่งผ่านเครื่องมือเช่น Zig AIR ซึ่งแสดงให้เห็นถึงความต้องการสำหรับการตรวจสอบความถูกต้องอย่างเป็นทางการทั่วทั้งระบบนิเวศการเขียนโปรแกรมระบบ
การแสวงหาความถูกต้องของโค้ดที่พิสูจน์ทางคณิตศาสตร์ยังคงดึงดูดความสนใจในชุมชนการเขียนโปรแกรมต่างๆ แม้ว่าจะมีความเข้าใจที่ละเอียดอ่อนมากขึ้นเกี่ยวกับสิ่งที่การตรวจสอบความถูกต้องอย่างเป็นทางการสามารถส่งมอบได้จริง เมื่อเครื่องมือพัฒนาขึ้นและแนวทางมีความหลากหลายมากขึ้น ช่องว่างระหว่างความสมบูรณ์แบบทางทฤษฎีและการใช้งานจริงค่อยๆ แคบลง แม้ว่าเป้าหมายที่จับต้องได้ยากของโค้ดที่ปราศจากข้อบกพร่อง 100% ยังคงเป็นความมุ่งมั่นมากกว่าความเป็นจริง