เครื่องมือตรวจสอบ Rust จุดประเด็นถกเถียงเรื่องวิธีการตรวจสอบแบบเป็นทางการกับการทดสอบ

การประกาศล่าสุดเกี่ยวกับ Verus เครื่องมือตรวจสอบแบบคงที่สำหรับโค้ด Rust ได้จุดประเด็นถกเถียงอย่างเข้มข้นในชุมชนนักพัฒนาเกี่ยวกับบทบาทของการตรวจสอบแบบเป็นทางการในภาษาโปรแกรมที่เน้นความปลอดภัยอยู่แล้ว ในขณะที่ Rust ได้รับความนิยมเพิ่มขึ้นเรื่อยๆ จากการรับประกันความปลอดภัยในการจัดการหน่วยความจำ เครื่องมืออย่าง Verus มีเป้าหมายที่จะยกระดับความถูกต้องของโค้ดไปอีกขั้นด้วยการพิสูจน์ทางคณิตศาสตร์ว่าโค้ดเป็นไปตามข้อกำหนดที่ตั้งไว้

ระบบนิเวศที่เติบโตของเครื่องมือตรวจสอบ Rust

Verus เข้าร่วมกับระบบนิเวศที่กำลังเติบโตของเครื่องมือตรวจสอบสำหรับ Rust ซึ่งรวมถึง Prusti และ Creusot ในขณะที่เครื่องมือเหล่านี้มีเป้าหมายร่วมกันในการตรวจสอบความถูกต้องของโค้ด แต่พวกมันใช้วิธีการแตกต่างกันในการแก้ปัญหา ตามที่ผู้แสดงความคิดเห็นคนหนึ่งได้กล่าวไว้ว่า เครื่องมือหลักๆ คือ Verus, Prusti และ Creusot แต่พวกมันใช้วิธีการที่แตกต่างกันมาก นี่ไม่ใช่ความซ้ำซ้อน ตามเอกสารวิจัย SOSP 2024 ที่อ้างถึงในความคิดเห็น ความเร็วในการตรวจสอบดูเหมือนจะเป็นข้อได้เปรียบหลักของ Verus เมื่อเทียบกับเครื่องมืออื่นที่คล้ายกัน

เครื่องมือเหล่านี้ช่วยให้นักพัฒนาสามารถเขียนข้อกำหนดว่าโค้ดของพวกเขาควรทำอะไร และจากนั้นตรวจสอบแบบคงที่ว่าโค้ดเป็นไปตามข้อกำหนดเหล่านั้นสำหรับการทำงานทั้งหมดที่เป็นไปได้ ต่างจากการทดสอบแบบดั้งเดิมที่สามารถตรวจสอบเฉพาะอินพุตที่กำหนด เครื่องมือตรวจสอบแบบเป็นทางการเช่น Verus สามารถพิสูจน์ความถูกต้องครอบคลุมทั้งพื้นที่อินพุต

การเปรียบเทียบเครื่องมือตรวจสอบความถูกต้องของ Rust

• Verus: เครื่องมือตรวจสอบแบบสถิตที่ตรวจสอบโค้ดเทียบกับข้อกำหนดสำหรับการทำงานทุกรูปแบบที่เป็นไปได้ ปัจจุบันรองรับ Rust บางส่วนและอนุญาตให้ตรวจสอบโค้ดที่จัดการกับพอยน์เตอร์แบบดิบ
• Prusti: เครื่องมือตรวจสอบอีกตัวสำหรับ Rust ที่มีวิธีการแตกต่างกัน
• Creusot: เครื่องมือตรวจสอบตัวที่สามในระบบนิเวศของ Rust
• Kani: ตัวตรวจสอบโมเดลที่กำลังถูกใช้เพื่อตรวจสอบไลบรารีมาตรฐานของ Rust

ประเด็นสำคัญในการอภิปราย:

• ความเร็วในการตรวจสอบเป็นตัวแบ่งแยกระหว่างเครื่องมือต่างๆ
• ความจำเป็นในการมีภาษาข้อกำหนดที่เป็นมาตรฐานร่วมกัน
• การบูรณาการกับระบบเอฟเฟกต์ที่กำลังจะมาถึงของ Rust
• การแลกเปลี่ยนระหว่างประเภทที่ขึ้นต่อกันแบบในตัวกับเครื่องมือตรวจสอบภายนอก

ภาพหน้าจอของพื้นที่เก็บข้อมูล GitHub สำหรับ Verus ที่แสดงให้เห็นถึงการพัฒนาและการมีส่วนร่วมอย่างต่อเนื่องภายในระบบนิเวศของเครื่องมือตรวจสอบ Rust

การถกเถียง: การตรวจสอบแบบเป็นทางการกับการทดสอบ

การประกาศนี้ได้จุดประเด็นถกเถียงเชิงปรัชญาว่าการตรวจสอบแบบเป็นทางการจำเป็นหรือไม่ในภาษาอย่าง Rust ที่มีการรับประกันความปลอดภัยที่แข็งแกร่งอยู่แล้ว นักพัฒนาบางคนตั้งคำถามว่าการเพิ่มเครื่องมือตรวจสอบบน Rust นั้นมากเกินไปหรือไม่ โดยโต้แย้งว่าการทดสอบควรเพียงพอสำหรับกรณีการใช้งานส่วนใหญ่

การทดสอบยืนยันว่าโค้ดทำงานบนอินพุตเฉพาะ การตรวจสอบแบบเป็นทางการตรวจสอบว่าโค้ดทำงานบนทุกอินพุต

มุมมองนี้เน้นความแตกต่างพื้นฐานระหว่างการทดสอบและการตรวจสอบ ในขณะที่การทดสอบสามารถแสดงให้เห็นว่าโค้ดทำงานสำหรับอินพุตบางอย่าง การตรวจสอบแบบเป็นทางการสามารถพิสูจน์ว่าโค้ดทำงานสำหรับอินพุตทั้งหมดที่เป็นไปได้ รวมถึงกรณีพิเศษที่อาจถูกมองข้ามในการทดสอบ

บทบาทของ Dependent Types

อีกประเด็นที่น่าสนใจในการสนทนาคือเรื่อง dependent types และควรจะรวมเข้าไปในตัวภาษาเองหรือไม่ Dependent types อนุญาตให้ประเภทขึ้นอยู่กับค่า ซึ่งช่วยให้สามารถกำหนดข้อกำหนดที่แม่นยำมากขึ้นในระดับประเภท อย่างไรก็ตาม ตามที่ผู้แสดงความคิดเห็นคนหนึ่งชี้ให้เห็น การเพิ่ม dependent types ให้กับ Rust อาจเพิ่มความซับซ้อนของระบบประเภทที่ซับซ้อนอยู่แล้วอย่างมีนัยสำคัญ

นักพัฒนาบางคนแสดงความกังวลว่าการทำให้การตรวจสอบแบบเป็นทางการเป็นส่วนหลักของ Rust อาจทำให้อุปสรรคในการเข้าถึงสูงเกินไป ตามที่ผู้แสดงความคิดเห็นคนหนึ่งอธิบายว่า: ความรู้สึกของผมคือ dependent types เพิ่มความซับซ้อนให้กับภาษาที่เป็นที่รู้จักกันดีอยู่แล้วว่ามีระบบประเภทที่ซับซ้อน ดังนั้นผมจึงกังวลเกี่ยวกับการเพิ่มงบประมาณความซับซ้อน พวกเขาแนะนำว่าการแยกเครื่องมือตรวจสอบออกไปช่วยให้นักพัฒนาที่ต้องการใช้งานสามารถใช้ได้โดยไม่ต้องสร้างภาระให้กับคนอื่นๆ ด้วยความซับซ้อน

ทิศทางในอนาคต: ภาษาข้อกำหนดร่วม

ประเด็นที่เกิดขึ้นซ้ำในความคิดเห็นคือความจำเป็นในการมีภาษาข้อกำหนดร่วมกันระหว่างเครื่องมือตรวจสอบต่างๆ เมื่อมีเครื่องมือหลายตัวเกิดขึ้นในพื้นที่นี้ นักพัฒนาแสดงความไม่พอใจที่ต้องเรียนรู้ไวยากรณ์ข้อกำหนดที่แตกต่างกันสำหรับงานตรวจสอบที่คล้ายกัน

การรับประกันอย่างง่าย เช่น การตรวจสอบว่าฟังก์ชันไม่เกิด panic อาจได้รับประโยชน์จากไวยากรณ์มาตรฐานในเครื่องมือตรวจสอบทั้งหมด ผู้แสดงความคิดเห็นบางคนแนะนำว่าการรับประกันพื้นฐานดังกล่าวอาจถูกรวมเข้าไปในภาษาหลักของ Rust ในที่สุด อาจเป็นส่วนหนึ่งของระบบเอฟเฟกต์ที่กำลังจะมาถึง (เดิมรู้จักในชื่อ keyword generics)

การสนทนายังเกี่ยวข้องกับความพยายามอย่างต่อเนื่องของ Rust ในการตรวจสอบไลบรารีมาตรฐานโดยใช้เครื่องมืออย่าง Kani ซึ่งเป็นเครื่องมือตรวจสอบโมเดล งานนี้แสดงให้เห็นถึงความสำคัญที่เพิ่มขึ้นของการตรวจสอบแบบเป็นทางการในการรับประกันความน่าเชื่อถือของโค้ดที่สำคัญ

ในขณะที่ Verus ยังคงพัฒนาและขยายความสามารถ มันเป็นก้าวสำคัญในการนำเทคนิคการตรวจสอบแบบเป็นทางการไปสู่นักพัฒนา Rust ในวงกว้าง แม้ว่าไม่ใช่ทุกโปรเจกต์จะต้องการระดับการรับประกันที่การตรวจสอบแบบเป็นทางการมอบให้ แต่การมีเครื่องมือเหล่านี้ช่วยเพิ่มความหลากหลายให้กับระบบนิเวศของ Rust และมอบทางเลือกเพิ่มเติมให้กับนักพัฒนาในการรับประกันความถูกต้องของโค้ด

อ้างอิง: Verus