Rust doğrulama teknolojisi, düşük seviye sistem kodunda uygulanıyor

Rust kodunun doğruluğunu doğrulamak için Verus aracı

• Verus, Rust ile yazılmış kodun doğruluğunu doğrulamak için bir araçtır.
• Geliştiriciler kodun yerine getirmesi gereken bir spesifikasyon yazar; Verus, çalıştırılabilir Rust kodunun tüm olası çalıştırmalarında bu spesifikasyonun her zaman karşılanıp karşılanmadığını statik olarak kontrol eder.
• Çalışma zamanı kontrolleri eklemek yerine, Verus güçlü bir çözümleyiciye güvenerek kodun doğru olduğunu kanıtlar.
• Verus şu anda Rust'ın bir alt kümesini destekler (geliştirme devam ediyor) ve kimi zaman geliştiricilere standart Rust tür sisteminin ötesinde, statik olarak kod doğruluğunu kontrol etme olanağı sağlar (ör. ham işaretçi manipülasyonu).

Verus'un güncel durumu

• Verus aktif olarak geliştiriliyor.
• Bazı özellikler bozulmuş veya eksik olabilir; belgeler de hâlâ eksiktir.
• Verus'ı denemek istiyorsanız, Zulip'te yardım isteyebilecek durumda olmalısınız.

Verus'u denemek

• Verus Playground'i ziyaret ederek Verus'u tarayıcıda deneyebilirsiniz.
• Daha karmaşık geliştirme için kurulum yönergelerini izleyin ve başlamak için Eğitim ve Referans ile aşağıdaki belgeleri inceleyin.

Verus belgeleri

• Eğitim ve Referans
• Verus standart kütüphanesi için API belgeleri
• Eşzamanlı kod doğrulaması için kılavuz
• Proje hedefi
• Verus'a katkı
• Lisans

İletişim kurma, hata bildirimi ve tartışma başlatma

• Sorunları GitHub'da bildirerek veya bir tartışma başlatarak, gerçek zamanlı tartışma ve yardım için Zulip'e üye olabilirsiniz.
• Mevcut özelliklerdeki gerçekleşebilir hatalar (bug'lar) için GitHub issue, özellik istekleri ve planlanan özellikler için daha açık bir tartışma yapmak üzere GitHub tartışmalarını kullanın.
• Katkılar memnuniyetle karşılanır; kod katkısı yapmak istiyorsanız Verus'a katkı için ipuçlarına bakın.

GN⁺'in görüşü

• Rust, sistem programlama için uygunluğu, güvenlik ve performansı sağlayan bir dil olarak iyi biliniyor; Verus ise bu Rust avantajlarını daha da güçlendiren bir proje gibi görünüyor. Özellikle eşzamanlı programlama doğrulaması özelliği oldukça ilginç görünüyor.

• Ancak proje hâlâ geliştirme sürecinin erken aşamasında ve desteklenen Rust sözdizimi sınırlı görünüyor; bu yüzden üretimde doğrudan kullanılabilmesi için daha fazla geliştirme gerekeceği anlaşılıyor. Yine de, kodun güvenliğini statik analizle önceden garanti altına almak önemlidir, bu nedenle gelecekte potansiyelinin yüksek olduğunu düşünüyorum.

• Geliştirme başlangıcında olduğu için hala yetersiz dokümantasyon ve sınırlı sözdizimi desteği gibi eksikler var; ancak uzun vadede Rust ekosisteminde önemli bir rol oynayacak gibi görünüyor. Özellikle sistem programlama veya blokzincir gibi güvenilirliğin kritik olduğu alanlarda kullanımının yüksek olmasını bekliyorum.

[GN⁺]

Hacker News Yorumu

• Verus ile resmi olarak doğrulanmış bir Kubernetes denetleyicisi yazıldı
  • Denetleyicinin sonunda istenen desired state ile kümeyi ayarlayacağını kanıtlayan bir liveness özelliği ispatlanabiliyor
  • Doğruluğu belirtirken çok fazla ince ayrıntı ve nüans var (desired state gereksinimlerinin hızla değişmesi, eşzamansızlık, arıza vb.)
  • Kod GitHub bağlantısında bulunuyor ve OSDI 2024'te yayımlanacak bir makaleye bağlı
• Verus için küçük bir adım olarak Rust'ın debug_assert ile önkoşul ve sonkoşul eklenebiliyor
  • Rust derleyicisi bunu varsayılan olarak üretim derlemelerinde kaldırır
  • Verus eğitimindeki örnekler ve debug_assert ile çalışma zamanı kontrol örnekleri sağlanıyor
• "Kod doğrulaması" ile "kodun doğruluğunun ispatı" arasındaki farkı soran bir acemi soru
  • CS/matematik geçmişi zayıf olan uygulama geliştiricileri için "kanıt" konusunda iyi bir eğitim materyali olup olmadığını merak ediyordum
  • "Sıfır bilgi" kanıtlarının neden önemli olduğunu ve neden bu kadar ilgili olduğunu çok merak ediyorum
• Rust standardı, C/C++, Common Lisp ve Ada/SPARK2014'te olduğu gibi henüz yok
  • Bu, Ada/SPARK2014 gibi diller için geliştirilmiş doğrulama araçlarıyla karşılaştırıldığında hareketli bir hedef
• Dafny, Rust'a derlenebilen bir "doğrulamaya duyarlı programlama dili"dir (GitHub bağlantısı)
• Başlıca katkı sağlayıcılardan biri, Zürih Rust Buluşması'nda Verus hakkında harika bir sunum yaptı (YouTube bağlantısı)
  • Program içinde ghost kodunun çok temiz oturduğu görüldü (biraz Ada'yı anımsatıyor)
• Verus ve SPARK karşılaştırması
  • Aynı genel sınıftan bir doğrulayıcı mı? Verus'nun Ada için değil Rust için bir doğrulayıcı olmasının dışında hangi farklar var?
• Verus konusunda uzman biri Verus ile Lean4'ün performans ve ifade gücünü karşılaştırabilir mi?
  • Verus'un SMT tabanlı bir doğrulama aracı, Lean'in ise hem etkileşimli bir kanıtlayıcı hem de SMT tabanlı bir araç olduğunu anlıyorum
  • Ancak biçimsel doğrulama konusundaki anlayışım sınırlı olduğu için, yazılım biçimsel tekniklerinde uzman birinden görüş almak daha iyi olurdu
• Verus ile Kani arasında bir bağ var mı? Farklı mı çalışıyorlar? (Kani GitHub bağlantısı)
• Çıktı kodunun hâlâ vanilla Rust araçlarıyla derlenebilen geçerli bir Rust kodu olması için bir uygulama yaklaşımı var mı?