Landskap pengesahan formal untuk bahasa pengaturcaraan terus berkembang, dengan alat seperti coq-of-rust bertujuan untuk membuktikan secara matematik ketepatan kod dalam aplikasi Rust. Walau bagaimanapun, perbincangan komuniti mendedahkan nuansa penting tentang apa yang boleh dan tidak boleh dijamin oleh pengesahan formal, bersama-sama dengan berita mengenai perubahan nama yang signifikan dalam ekosistem pengesahan.
Realiti Tuntutan Pengesahan Formal
Walaupun coq-of-rust menjanjikan untuk menghasilkan aplikasi tanpa pepijat melalui pembuktian matematik, komuniti pembangun telah menekankan perbezaan penting. Pengesahan formal membuktikan bahawa kod melaksanakan spesifikasi dengan betul, tetapi tidak dapat menjamin bahawa spesifikasi itu sendiri bebas daripada kecacatan.
Saya menyukai pengesahan formal. Tetapi saya menganggap ini sebagai gambaran yang salah tentang apa yang ditawarkannya. Ia membolehkan anda membuktikan secara matematik bahawa kod anda melaksanakan spesifikasi dengan betul. Ia tidak membuktikan bahawa spesifikasi anda bebas daripada pepijat & kerentanan. Ia tidak membuktikan bahawa spesifikasi anda melaksanakan peraturan perniagaan anda dengan betul.
Perbezaan antara pengesahan (adakah kod sepadan dengan spesifikasi?) dan validasi (adakah spesifikasi sepadan dengan keperluan sebenar?) mewakili konsep asas dalam jaminan kualiti. Pengesahan formal cemerlang dalam membuktikan invariant berlaku untuk semua input yang mungkin, yang sangat berharga di mana spesifikasi lebih mudah daripada pelaksanaan, seperti dalam pangkalan data dan sistem fail.
Coq Menjadi Rocq: Penjenamaan Semula yang Signifikan
Perkembangan penting yang disebut dalam komen ialah pembantu bukti Coq, asas coq-of-rust, telah dinamakan semula kepada Rocq. Menurut perbincangan komuniti, perubahan ini adalah hasil daripada tinjauan komuniti di mana kira-kira 24% pengguna menyatakan ketidakselesaan dengan nama asal, mendapati ia tidak selesa atau janggal untuk digunakan dalam persekitaran profesional. Projek ini kini dikenali secara rasmi sebagai Rocq dan boleh didapati di rocq-prover.org.
Penjenamaan semula ini telah mencetuskan reaksi bercampur-campur, dengan sesetengah melihatnya sebagai evolusi profesional yang diperlukan sementara yang lain menyesali kehilangan apa yang mereka anggap sebagai permainan kata yang tidak berbahaya.
Kedudukan Unik Rust dalam Pengesahan
Model ingatan mutable-xor-aliased Rust menjadikannya sangat sesuai untuk pengesahan formal berbanding dengan banyak bahasa lain. Model ini, di mana data boleh sama ada boleh diubah atau mempunyai beberapa rujukan tetapi tidak kedua-duanya secara serentak, mewujudkan asas yang boleh dibina oleh alat pengesahan dengan lebih berkesan.
Ahli komuniti menyatakan bahawa tanpa model seperti itu, pengesahan menjadi sama sukar — dan sama tidak praktikal — seperti semua pengesah untuk bahasa yang sedia ada. Ini memberikan alat pengesahan berasaskan Rust seperti coq-of-rust, Verus, dan lain-lain kelebihan yang berpotensi dalam ruang pengesahan.
Alat Pengesahan Formal untuk Rust yang Disebut dalam Komen
- coq-of-rust: Menterjemahkan Rust kepada Coq untuk pengesahan formal
- Verus: Bertujuan untuk pengesahan sistem penuh (sistem fail yang disahkan, pengawal Kubernetes)
- Creusot: Penterjemahan dari MIR kepada Why3 (dan kemudian penyelesai SMT)
- Ironclad/Gloire: Bukan khusus untuk Rust, tetapi kernel OS yang disahkan secara formal yang ditulis dalam SPARK/Ada
Perkara Utama Tentang Pengesahan Formal
- Membuktikan kod melaksanakan spesifikasi dengan betul
- Tidak membuktikan spesifikasi itu sendiri adalah betul
- Sangat berguna apabila spesifikasi lebih mudah daripada pelaksanaan
- Mendapat manfaat daripada model memori "mutable-xor-aliased" Rust
Pendekatan Alternatif dan Pesaing
Landskap pengesahan formal melampaui coq-of-rust. Ahli komuniti menyoroti beberapa alternatif, termasuk Verus untuk pengesahan sistem (digunakan dalam sistem fail yang disahkan dan pengawal Kubernetes), dan kernel Ironclad dengan Gloire OS yang dibina di atasnya menggunakan SPARK dan Ada.
Sesetengah pembangun menyatakan minat untuk melihat pendekatan pengesahan yang serupa digunakan untuk bahasa lain seperti Zig, khususnya melalui alat seperti Zig AIR, mencadangkan minat terhadap pengesahan formal di seluruh ekosistem pengaturcaraan sistem.
Usaha untuk membuktikan ketepatan kod secara matematik terus menarik minat di seluruh komuniti pengaturcaraan, walaupun dengan pemahaman yang lebih halus tentang apa yang boleh diberikan oleh pengesahan formal secara realistik. Apabila alat semakin matang dan pendekatan semakin pelbagai, jurang antara kesempurnaan teori dan pelaksanaan praktikal semakin mengecil, walaupun matlamat yang sukar dicapai iaitu kod 100% bebas pepijat masih lebih kepada aspirasi daripada realiti.