Lanskap verifikasi formal untuk bahasa pemrograman terus berkembang, dengan alat seperti coq-of-rust yang bertujuan untuk membuktikan secara matematis kebenaran kode dalam aplikasi Rust. Namun, diskusi komunitas mengungkapkan nuansa penting tentang apa yang dapat dan tidak dapat dijamin oleh verifikasi formal, bersamaan dengan berita perubahan nama yang signifikan dalam ekosistem verifikasi.
Realitas Klaim Verifikasi Formal
Meskipun coq-of-rust menjanjikan untuk membuat aplikasi tanpa bug melalui pembuktian matematis, komunitas pengembang telah menyoroti perbedaan penting. Verifikasi formal membuktikan bahwa kode mengimplementasikan spesifikasi dengan benar, tetapi tidak dapat menjamin bahwa spesifikasi itu sendiri bebas dari cacat.
Saya menyukai verifikasi formal. Tetapi saya menganggap ini sebagai kesalahpahaman tentang apa yang ditawarkannya. Verifikasi formal memungkinkan Anda membuktikan secara matematis bahwa kode Anda mengimplementasikan spesifikasi dengan benar. Ini tidak membuktikan bahwa spesifikasi Anda bebas dari bug & kerentanan. Ini tidak membuktikan bahwa spesifikasi Anda mengimplementasikan aturan bisnis Anda dengan benar.
Perbedaan antara verifikasi (apakah kode sesuai dengan spesifikasi?) dan validasi (apakah spesifikasi sesuai dengan kebutuhan sebenarnya?) merupakan konsep fundamental dalam jaminan kualitas. Verifikasi formal unggul dalam membuktikan invariant berlaku untuk semua input yang mungkin, yang sangat berharga ketika spesifikasi lebih sederhana daripada implementasi, seperti dalam database dan sistem file.
Coq Menjadi Rocq: Perubahan Nama yang Signifikan
Perkembangan penting yang disebutkan dalam komentar adalah bahwa asisten pembuktian Coq, dasar dari coq-of-rust, telah berganti nama menjadi Rocq. Menurut diskusi komunitas, perubahan ini dihasilkan dari survei komunitas di mana sekitar 24% pengguna menyatakan ketidaknyamanan dengan nama asli, menganggapnya tidak nyaman atau canggung untuk digunakan dalam lingkungan profesional. Proyek ini sekarang secara resmi dikenal sebagai Rocq dan dapat ditemukan di rocq-prover.org.
Perubahan nama ini menimbulkan reaksi beragam, dengan beberapa memandangnya sebagai evolusi profesional yang diperlukan sementara yang lain menyesalkan hilangnya apa yang mereka anggap sebagai permainan kata yang tidak berbahaya.
Posisi Unik Rust dalam Verifikasi
Model memori mutable-xor-aliased dari Rust membuatnya sangat cocok untuk verifikasi formal dibandingkan dengan banyak bahasa lain. Model ini, di mana data dapat berupa mutable atau memiliki beberapa referensi tetapi tidak keduanya secara bersamaan, menciptakan fondasi yang dapat dibangun oleh alat verifikasi secara lebih efektif.
Anggota komunitas mencatat bahwa tanpa model seperti itu, verifikasi menjadi sama sulitnya — dan sama-sama tidak praktis — seperti semua verifikator untuk bahasa yang ada. Ini memberikan alat verifikasi berbasis Rust seperti coq-of-rust, Verus, dan lainnya keunggulan potensial dalam ruang verifikasi.
Alat Verifikasi Formal untuk Rust yang Disebutkan dalam Komentar
- coq-of-rust: Menerjemahkan Rust ke Coq untuk verifikasi formal
- Verus: Bertujuan untuk verifikasi sistem penuh (sistem berkas terverifikasi, pengontrol Kubernetes)
- Creusot: Penerjemahan dari MIR ke Why3 (dan kemudian ke pemecah masalah SMT)
- Ironclad/Gloire: Tidak spesifik untuk Rust, tetapi kernel OS yang diverifikasi secara formal yang ditulis dalam SPARK/Ada
Poin Penting Tentang Verifikasi Formal
- Membuktikan kode mengimplementasikan spesifikasi dengan benar
- Tidak membuktikan bahwa spesifikasi itu sendiri benar
- Sangat berguna ketika spesifikasi lebih sederhana daripada implementasi
- Mendapat manfaat dari model memori "mutable-xor-aliased" milik Rust
Pendekatan Alternatif dan Pesaing
Lanskap verifikasi formal meluas di luar coq-of-rust. Anggota komunitas menyoroti beberapa alternatif, termasuk Verus untuk verifikasi sistem (digunakan dalam sistem file terverifikasi dan pengontrol Kubernetes), dan kernel Ironclad dengan Gloire OS yang dibangun di atasnya menggunakan SPARK dan Ada.
Beberapa pengembang menyatakan ketertarikan untuk melihat pendekatan verifikasi serupa diterapkan pada bahasa lain seperti Zig, khususnya melalui alat seperti Zig AIR, menunjukkan adanya minat untuk verifikasi formal di seluruh ekosistem pemrograman sistem.
Upaya untuk membuktikan kebenaran kode secara matematis terus menarik minat di berbagai komunitas pemrograman, meskipun dengan pemahaman yang lebih bernuansa tentang apa yang secara realistis dapat diberikan oleh verifikasi formal. Seiring dengan kematangan alat dan diversifikasi pendekatan, kesenjangan antara kesempurnaan teoretis dan implementasi praktis secara bertahap menyempit, meskipun tujuan yang sulit dicapai dari kode 100% bebas bug tetap lebih merupakan aspirasi daripada kenyataan.