Güzel yazı. Daha önce program doğrulama yapmış biri olarak Rust, biçimsel yöntemleri uygulamak için en kullanışlı modern dil gibi görünüyor.
Rust’ın kuralları, biçimselleştirmesi zor olan birçok durumu ortadan kaldırıyor. Geriye kalan büyük sorun, thread bakış açısından ve Rc/ödünç alma bakış açısından deadlock analizi; ikisi bir ölçüde eşdeğer. Rust’ta statik deadlock analizi olsaydı güvenli ters başvuru işaretçileri de mümkün olabilir gibi; tüm borrow/upgrade çağrılarının başarısız olmayacağını kanıtlayabilirsek referans sayaçlarının çoğunu ortadan kaldırabiliriz. Böylece mümkün olan durumlarda içsel değiştirilebilirliği de bedavaya elde ederiz.
Teorem kanıtlayıcıların büyük sorunu, teorem kanıtlamayı seven kişiler tarafından yapıldıkları için biçimciliğe saplanmaları ve programcılarla UI hissiyatlarının uyuşmaması. Kanıt yükümlülüklerinin çoğu SAT çözücüyle halledilebilir, ama zor problemler için daha ağır araçlar gerekiyor. Coq fazla elle işlem gerektiriyor; yazar ACL2’nin de fazla işlevsel olduğunu düşünüyor. Makine öğrenmesi, teorem kanıtlayıcılara yön göstermede yardımcı olabilir. Kanıtın kendisini ona bırakmak zor, ama kontrol akışı ve veri kullanımı çoğunlukla benzer olan kodlarda kanıt planlarını çıkarsamak mümkün görünüyor.
F*, otomatik kanıt sağlayan efsanevi bir dile yakın. SAT’tan daha güçlü SMT çözücüleri kullanıyor; otomatik çözüm başarısız olursa elle kanıt da mümkün.
Firefox ve Wireguard’ın kripto rutinleri Rust ile değil, F* ile; daha doğrusu F* içine gömülü düşük seviyeli DSL olan Low* ile yazıldı ve tamamen doğrulanmış durumda. https://project-everest.github.io/ https://mitls.org/
Katılıyorum, ancak Lean’in zengin metaprogramlama olanakları sayesinde etkileşimli teorem kanıtı doğrulamasının kullanıcı deneyiminde büyük ilerleme kaydettiğini düşünüyorum.
Böyle araçları Rust gibi harici dillerin doğrulanmasına uygularken sorun, kanıtların hedef dilde yazılmaması ve geliştiricinin iki dili birden öğrenmek zorunda kalması. Creusot’u yazarken edindiğim deneyime, Verus ve Aeneas üzerindeki çalışmalara ve Why3 laboratuvarı deneyimine dayanarak “doğrulamayı gözeten Rust”ın nasıl görünebileceğini düşünüyordum. Böyle bir dil baştan tasarlanırsa, Rust’a kıyasla doğrulanabilirlik kademeli olarak daha da iyileşebilir; özellikle de kanıtın zor kısımlarında etkisi büyük olabilir.
Coq/Agda/Lean ailesinin kanıt alanında kazanan olacağını düşünüyorum. Etkileşim, geri bildirim döngüsü olarak oldukça iyi bir model; ayrıca bu sistemler zaten var ve gerçekten çalışıyor.
Yerleşik özellik olarak en çok eksikliğini hissettiğim şey, “kanıtım üzerinde quickcheck çalıştır” karşılığı bir özellik. Kod elinizdeyken doğru olmayan bir özelliği kanıtlamaya çalışıp kanıtın neden ilerlemediğini anlamaya çalışırken saç baş yolmak kolay. Kanıtın ortasında anlamsız bir duruma ulaşıldığında “buradan bir karşı örnek üret” gibi bir komutun karşı örnek dökmesi iyi olurdu. Kanıtlar büyük ölçüde yol bağımlı ve genelde kolay değil, ama bu araçlar büyüklüğe çok yakın görünüyor. Kodu kanıtlama süreci, o kodun bug barındırabileceği olasılığını da yansıtmalı.
Makine öğrenmesinin teorem kanıtlayıcıya rehberlik etmesi ilginç bir fikir. Makine öğrenmesi sistemi doğruysa geçerli bir kanıta götürerek büyük kazanç sağlar; yanlışsa da büyük bir kayıp yoktur.
Kanıtlayıcı yanlış bir kanıt üretmez, sadece geçerli bir kanıt çıkarma konusunda başarısız olur. Bu özelliğe sahip makine öğrenmesi uygulamasının çok olmadığını düşünüyorum.
Biçimsel doğrulama uzmanı değilim, ama geleneksel anlamdaki lockların pek yardımcı olmadığını düşünüyorum. Hiçbir derleyici lock’lar hakkında işe yarar bir şey sunmuyor; sadece riski kabullenip yaşamak gerekiyor.
Aslında Rust’ta lock’lar ve referans sayaçları çalışma zamanı yapılarıdır. Arc, Rust’ın RAII modelini ciddi biçimde bozdu; bu yüzden kapsam bitmeden önce yıkıcının çalışması gereken scoped thread’ler kaldırılmak zorunda kaldı. Küresel referans sayaçlarında döngü ve sızıntı sorunları var ve bu yeniden küresel bir probleme dönüşüyor. Tamamen ortadan kaldırmak zor olabilir, ama arena tarzı kapsamlarla sınırlamanın daha iyi olduğuna inanıyorum. Lock’lar için kanal gibi asimetrik veri yapıları gerekiyor gibi görünüyor. Go’da kanallar gönderici ve alıcı olarak ayrılır; gönderici goroutine’de defer close(ch) koyabilirsiniz ve panic olsa bile thread’in geri kalanı bittiğinde çalışması garanti edilir. Mutlaka kanal olmak zorunda değil, ama okuma-yazma/üretici-tüketici rollerini ayırmak çıkarımı çok daha kolaylaştırır ve biçimsel analize de yardımcı olur gibi görünüyor.
Hoare’ın 1973 civarındaki makalesinden yapılan alıntıyla başlayıp şimdi ikinci yazıya kadar gelmesini seviyorum. Aslında boat’ın yazısının HN başlığında uzun bir yorum yazmış, bu alıntıyı Rust merkezli bir bakış açısına kaydırmanın boat’ın geçmişi düşünüldüğünde anlaşılır olduğunu, ama Hoare eleştirisinin kapsamını yapay biçimde daralttığını söylemiştim.
Şimdi Grayson bu dar parçayı başlangıç noktası alıp Rust’ın birkaç ilginç alanını ve tasarım noktasını tartışmış. Hâlâ kendi yorumumun doğru olduğunu düşünüyorum, ama Grayson’ın yazısından doğan tartışma, çıkış noktası olan yazıya yönelik teknik itirazlarımı dengelemeye yetecek kadar iyiydi.
1990’ların ortalarına gelindiğinde Hoare’ın kendisi de 1970’ler tarzı sağlamlık odaklı yaklaşımın temellerinde bir şeylerin yanlış olabileceğini zaten fark etmişti: http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h...
Ondan sonra basit testlerden daha gelişmiş sağlam olmayan teknikler ortaya çıktıkça, sağlam olmayan yöntemlerin sağlam yöntemlerin önüne geçtiğini düşünüyorum.
1973, 50 yıl öncesi; bir uzmanın tüm meslek ömrü demek. Hoare gerçekten çok yaklaşmıştı.
Sorunu tespit etmişti ve geriye dönüp bakınca, bir tip sistemiyle paylaşımlı XOR değiştirilebilirliği zorunlu kılma çözümü küçük bir adım gibi görünüyor. O zaman o küçük adımın çözüm olduğunu anlayabilseydik, 50 yıllık muazzam acıyı azaltmış olurduk.
boat’ın Hoare makalesi alıntısı hakkında o zaman yazdığım düşünce şuydu. Hoare’ın ilk alıntısından ve kısa girişten sonra yazar, “Tony Hoare referansların jump’lar gibi olduğunu söylediğinde ele aldığı şey, değiştirilebilir ve alias’lı durum problemiydi” diyor. withoutboats tanınmış bir Rust geliştiricisi olduğu için bu yorum şaşırtıcı değil.
Ama alıntının kendisinin bu bakış açısını güçlendirdiğini sanmıyorum. Hoare’ın daha genel olarak referansların semantik varlığının kendisinden yakınmasını alıp Rust’ın alias’sız değiştirilebilir durum modeline uygulayarak sorunu etrafından dolaşma girişimi olarak görülebilir. Ancak bu, daha büyük bir sorunun yalnızca dar bir parçasını düzeltip tüm sorun ortadan kalkmış demeye daha yakın. Eksik bırakılan kısımlar, özellikle “Variables” bölümünün başı ve ALGOL 68 örneği, Hoare’ın yalnızca değiştirilebilir durumu değil, referans adlı semantik kavramın kendisini eleştirdiği yönüne çok daha güçlü biçimde işaret ediyor. Rust’ın sorunun bir kısmını ehlileştirme girişimini kabul ediyorum, ama hiçbir dilin bu sorunu “düzelttiğini” düşünmüyorum.
Bu yazıya neden bu kadar çok övgü geldiğini pek anlamıyorum. Program analizinin birçok alanını tek bir paragrafla geçiştiriyor gibi. Graydon’ı seviyorum ve bakış açısına saygı duyuyorum, ama bu paragraf fazlasıyla basitleştirilmiş.
GC’li dillerin güçlü yerel akıl yürütme desteğini özellikle sağlamadığı şeklindeki açıklama bir korkuluk safsatası. Pony gibi, tip sisteminde bölgeler bulundurup yine de GC kullanan diller vardı. Ayrıca pointer analizi ve kaçış analizi diye koca alanlar var; benzersizliği çıkarımlar ve iki referansın alias olup olamayacağını belirlerler. Statik tiplerin özü de sınıf ve alan teknikleriyle heap’i birbirine alias olmayan parçalara ayırmaktır. Bu JavaScript meselesi değil; Java/C#/Scala ve sayısız GC dilinde değiştirilebilir durum hakkında yerel akıl yürütme yokmuş gibi davranılmamalı.
Genel durumda bunu otomatik olarak eksiksiz yapmak mümkün değil; pratikte ayırma mantığına oldukça benzeyen bir şeye ihtiyaç var. Rust’ın borrow checker semantiği de basitleştirilmiş bir ayırma mantığı türü olarak görülebilir.
Sınıflar ve alanlar, değiştirilebilir durum hakkında tam bir yerel akıl yürütme sağlamaz. Çünkü sınıf/nesne A, sınıf/nesne B’nin değiştirilebilir durumuna bağımlı hâle gelebilir. Java tarzı sınıf kalıtımı da program zamanla evrildikçe kendi başına daha fazla karmaşıklık ekler.
Graydon, GC’nin güçlü yerel akıl yürütmeyi imkânsız kıldığını söylemiyor. Sebebi ne olursa olsun çoğu dil tasarımcısının bu hedefin tersine seçimler yaptığını söylüyor; bu da açıkça doğru görünüyor.
Elbette karşı örnekler var, ama Java, C#, Python gibi ana akım GC’li genel amaçlı dillere bakınca doğru. Nesne yönelimliliğin ilk fikrinin bugünkü aktör modeline yakın olduğu ve sahiplenilmiş veri yapılarını yalnızca mesaj iletimiyle değiştirmeye çalıştığı yorumu yapılabilir. Fakat gerçek dünyadaki nesne yönelimli uygulamalar bu hedefe pek yaklaşmıyor. Java, aynı nesneye yönelik değiştirilebilir referansların birden çok nesnede saklanmasını engellemez. Bu yazı bunu daha iyi açıklıyor: https://without.boats/blog/references-are-like-jumps/
Küçük bir test: Bu kod ne yazdırır? void myMethod(final Map map) { map.remove("key"); int oldSize = map.size(); map.put("key", "val"); int newSize = map.size(); System.out.println(newSize - oldSize); }
Düzenleme: Çifte olumsuzlamayı yanlış okumuşum. Tekrar okuyunca hâlâ kafa karıştırıcı. Java’da, JavaScript’ten farklı olarak yerel akıl yürütme olduğu mu kastediliyor?
Graydon’ın yazılarını genelde severim, ama bu yazı, pek çok biçimsel yöntem yazısı gibi alanı bilmeyen okurları yanlış yönlendirebilir. Kurşunu altına çevirmenin yönteminde tek haneli mertebede bir iyileşme olduğunu söyleyip, pratik maliyet etkinliğine ulaşmak için hâlâ 29 haneli mertebede yol kaldığını söylememeye benziyor. Alias olmaması biçimsel doğrulamayı çok daha kolaylaştırır mı? Evet. Peki bu, gerçek dünyadaki programları pratik ve maliyet etkin biçimde doğrulayabileceğimiz anlamına mı gelir? Kesinlikle hayır. Her gün biçimsel olarak doğrulanan programlar, devreler ve bileşenler var; ama bunlar istisna niteliğinde, görece çok küçük ve özel olarak dikkatli bir yöntemle geliştiriliyor. Yerel akıl yürütmeye yardımcı olan özellikler önemlidir, fakat ana akım yazılımların doğruluğunu sağlam bir yöntemle garanti etme biçiminde kayda değer bir değişiklik yaratmaz.
Heap’i, pointer’ı, integer’ı olmayan; yalnızca boolean değişkenleri bulunan ve döngüleri ikiden fazla dönemeyen, Turing-tam olmaktan uzak bir dildeki programlar bile TQBF’ye indirgenebildiği için pratikte doğrulanamaz. Bazı özellikler, örneğin bellek güvenliği için bu mümkün olabilir; ama yazılımın ihtiyaç duyduğu şeyler için yeterli değildir. 1970–90’larda, en kötü durum karmaşıklığı yönetilemez olsa bile dilin yerel garantileri ve yapısının bizi en kötü durumdan uzaklaştıracağı umudu vardı; ancak sonrasında bunun böyle olmadığı kanıtlandı. İnsanların gerçekten yazdığı programların en kötü durumdan iyi sezgiseller çıkaracak kadar uzak olduğu umudu da artık pek geçerli görünmüyor.
Bununla ilgili bir sunum var: https://pron.github.io/posts/correctness-and-complexity
Temel sonuç şu: Doğrulamak isteyeceğiniz ilginç özelliklerin çoğu bileşmez. P1...Pn bileşenlerinin her biri için bir özelliği kanıtlasanız bile, P1 ○ ... ○ Pn için o özelliği kanıtlamanın maliyeti yalnızca n’e göre süper-polinom biçimde artmakla kalmaz, her bir bileşenin boyutuna göre de süper-polinom artar. Yani parçalamadığınız zamanki kadar zordur; doğruluk ayrıştırılamaz. Bu yüzden “epey çok şeyi doğrulayabiliriz” ile “doğrulanabilenler denizde bir damladır” aynı anda doğrudur ve biçimsel yöntem tartışmalarında bu uçurum sık sık atlanır.
Son 6 yıldan uzun süredir HN’de aynı argümanı yüzlerce kez tekrarladın ve bu süreçte aldığın çok sayıdaki yorumdan sonra bile neredeyse hiç nüans eklenmedi.
Tamamen yanlış değil, ama tamamen doğru da değil. Bu konuyla ilgilenen pek çok kişinin, yüzlerce tekrar içinde bunu gösterme fırsatı bolca olmuşken görüşünün hiç evrilmemiş olması şaşırtıcı. Bu tutum hastalıklı bir kapalılık gibi duyuluyor ve tartışmaya katılan herkesin zamanını boşa harcatıyor.
Sağlamlığa odaklanmanın, daha doğru yazılım hedefine yardımcı olmaktan ziyade, pratikte daha iyi sonuç veren tekniklerden dikkati uzaklaştırdığını düşünüyorum. Teorik olarak da desteklenen pratik teknikler var ve sağlamlığın tek yol olduğunu düşünenleri bazen şaşırtabiliyor: http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h...
Bu tekrar tekrar oluyor. Sağlam yöntemlerde önemli iyileştirmeler olurken bile, sağlam olmayan yöntemler pratikte daha doğru yazılıma doğru çok daha büyük ilerleme sağladı. Çok yakın tarihli bir örnek olarak https://antithesis.com var. Elbette belirli durumlarda sağlam teknikler daha güçlü ve pratik olabilir; bu karmaşık bir konu.
Küçük Rust kütüphanelerinin unsafe kullanımını doğru yapıp yapmadığını doğrulayabilir hâle gelmeyi beklemek makul. Bu tek başına bile gerçekten faydalı.
F* yazısına da az önce ilgili bir yorum bıraktım. Söz dizimine bakınca öznel olarak Rust yerine F*/F#’ı tercih ediyorum, ancak geliştirmekte olduğum gösteri kontrol yazılımında Ada/SPARK2014 kullanmaya karar verdim.
Rust’ın Ada/SPARK2014 ile aynı tür insanları çekebilmesi için C, Common Lisp, Prolog, Fortran, COBOL gibi mevcut dillerde olduğu gibi resmî yayımlanmış bir standarda ihtiyacı var. AdaCore ile Ferrous Systems, Ada/SPARK2014’tekine benzer şekilde Rust için biçimsel doğrulama araçları sunmak üzere iş birliği yaparken Rust da bu alana giriyor; ancak henüz yayımlanmış bir standardı yok ve Ada ile SPARK2014’ün mirası çok büyük.
Referans sayımını, kesin biçimde çevrimsiz verilere uygulandığında ya da döngüsel sızıntıları göze alabildiğinizde çalışan, bir tür hemen çalıştırılan optimize GC olarak görebilmek ilginç. Python, yazıda anlatılan referans sayımı + izleme karması yaklaşımı kullanır; izleme toplayıcısını yalnızca her N istekte bir çalışacak şekilde zorlayan üretim dağıtımları da gördüm
Perl saf referans sayımı kullanır ama zayıf referanslara sahip olduğu için, döngüsel yapının hangi kısmının referansını tuttuğunuza dikkat etme pahasına veriyi referans sayımı açısından çevrimsiz hâle getirebilirsiniz. Koka teoride referans sayımı kullanır, ama pratikte bunu mümkün olduğunca derleme zamanına taşımaya çalışır; y = x + 1 içinde x için yalnızca tek referans olduğu ve sonrasında kullanılmadığı garanti edilebiliyorsa, y için aynı depolamayı yeniden kullanıp yerinde değişiklik yapabilir
Nim, ORC sunar; bu, otomatik referans sayımına Bacon+Rajan’ın Recycler algoritmasının uygulanmasının eklenmiş hâlidir. Bu algoritma, referans sayımı tabanlı sistemlerde yalnızca döngüleri toplamak üzere tasarlandığından oldukça hızlıdır. Rust tarafına dönersek, stop-the-world Recycler uygulaması burada: https://github.com/fitzgen/bacon-rajan-cc ve bu fork’ta bacon-rajan-ccc crate’i olarak yayımlanıyor: https://github.com/mbartlett21/bacon-rajan-cc README’deki Alternative bölümünde aynı alandaki başka deneylere bağlantılar var. Recycler makalesini bulmak zorsa, kopyalarını https://trout.me.uk/gc/ altında topladım; benzer zevklere sahipseniz https://trout.me.uk/lisp/ altındaki makalelerden de keyif alabilirsiniz
Firefox da C++ DOM nesneleri ile JS üzerinden oluşan döngüleri yönetmek için referans sayımını trial deletion tabanlı döngü toplayıcı ile birlikte kullanır. Hatta ilk uygulamayı Graydon üstlenmişti
Programların biçimsel doğrulaması konusunda sabırsızlık hissediyorum. Bir programın belirtimi doğru uyguladığını kanıtlamak teorik olarak ilginç, ama pratikte pek işe yaramıyor
Doğru belirtim yazmak, doğru programlama kadar zor olduğundan, zor problem çözülmüyor; yalnızca başka yere taşınıyor. Biçimsel yöntemlerin pratik kullanım alanları var, ama bunlara nadiren rastlanıyor
Tam bir belirtim için bu doğru, ama asıl hedef genellikle bu değil. Çoğu zaman kanıtlamak istediğiniz şey birkaç temel özelliktir. Örneğin bu fonksiyonun her zaman sonlanması ya da şu fonksiyonun her zaman sıralı bir dizi döndürmesi gibi
Bunları yapabildiğinizde önkoşul olarak zorunlu kılabilirsiniz. Örneğin bir fonksiyona dizi geçmeden önce o dizinin önceden sıralanmış olduğunu göstermeniz gerekmesi gibi
15 Mayıs 2024’te yazılmıştı; o gün Rust 1.0’ın 9. yıl dönümüydü
Bağlantısı verilen Boats yazısını okudum ve harikaydı. Hoare’ın 50 yıl önceki alıntısının hâlâ ilgili olması ve ifadesinin de çok iyi olması şaşırtıcıydı
Daha basit bir yaklaşımla derleme zamanı type guard benzeri şeyler kullanabilmek isterdim. trait bound’lar çoğalınca tip düzeyi programları okumak zorlaşıyor
Örneğin Where <<::Output as G>::Output as H>::Output: HList + Z ya da type Output = <<::Output as G>::Output as H>::Output; gibi. Buna Cons>>> ekliyorsunuz ve TypeNum’daki U8 gibi sayıların bile aslında kendi içinde Cons>> iç içe geçmesi olduğunu fark ediyorsunuz. Bu alanda ilerleme kaydedip istenen doğrulamayı yaptırmak mümkün, ama hata mesajları insan geliştiricilerin kod yazma biçiminden çok farklılaşabiliyor ve uygulaması da çok sancılı oluyor
Geliştirici deneyiminin şaşırtıcı olmasının nedeni bunun “sadece bir fonksiyon” değil, belirli generic’ler ve ilişkili tiplerin bir birleşimi olması. Çalışma zamanı tarzı kontroller kullanıp bunları derleme zamanında çalıştırmak istiyorum, ama bunu yapmak için epey farklı kod yazmam gerekti. Sonuçta tip düzeyi derleme zamanı Rust’ını daha basit, fonksiyonel ve okunabilir kılmak, bu tür biçimsel analiz projelerinin bakımcılar ve kullanıcılar için iyi bir deneyim sunmasının yolu olabilir. Özetle comptime Rust istiyorum. Ayrıca Pin<&mut Self> tabanlı Future’ın şimdiden yerleşip yerleşmediğini de merak ediyorum. async/await için farklı iç uygulamaları denemek isterdim, ama nereden başlayacağımı bilmiyorum
1 yorum
Hacker News yorumları
Güzel yazı. Daha önce program doğrulama yapmış biri olarak Rust, biçimsel yöntemleri uygulamak için en kullanışlı modern dil gibi görünüyor.
Rust’ın kuralları, biçimselleştirmesi zor olan birçok durumu ortadan kaldırıyor. Geriye kalan büyük sorun, thread bakış açısından ve
Rc/ödünç alma bakış açısından deadlock analizi; ikisi bir ölçüde eşdeğer. Rust’ta statik deadlock analizi olsaydı güvenli ters başvuru işaretçileri de mümkün olabilir gibi; tüm borrow/upgrade çağrılarının başarısız olmayacağını kanıtlayabilirsek referans sayaçlarının çoğunu ortadan kaldırabiliriz. Böylece mümkün olan durumlarda içsel değiştirilebilirliği de bedavaya elde ederiz.Teorem kanıtlayıcıların büyük sorunu, teorem kanıtlamayı seven kişiler tarafından yapıldıkları için biçimciliğe saplanmaları ve programcılarla UI hissiyatlarının uyuşmaması. Kanıt yükümlülüklerinin çoğu SAT çözücüyle halledilebilir, ama zor problemler için daha ağır araçlar gerekiyor. Coq fazla elle işlem gerektiriyor; yazar ACL2’nin de fazla işlevsel olduğunu düşünüyor. Makine öğrenmesi, teorem kanıtlayıcılara yön göstermede yardımcı olabilir. Kanıtın kendisini ona bırakmak zor, ama kontrol akışı ve veri kullanımı çoğunlukla benzer olan kodlarda kanıt planlarını çıkarsamak mümkün görünüyor.
Firefox ve Wireguard’ın kripto rutinleri Rust ile değil, F* ile; daha doğrusu F* içine gömülü düşük seviyeli DSL olan Low* ile yazıldı ve tamamen doğrulanmış durumda.
https://project-everest.github.io/
https://mitls.org/
Böyle araçları Rust gibi harici dillerin doğrulanmasına uygularken sorun, kanıtların hedef dilde yazılmaması ve geliştiricinin iki dili birden öğrenmek zorunda kalması. Creusot’u yazarken edindiğim deneyime, Verus ve Aeneas üzerindeki çalışmalara ve Why3 laboratuvarı deneyimine dayanarak “doğrulamayı gözeten Rust”ın nasıl görünebileceğini düşünüyordum. Böyle bir dil baştan tasarlanırsa, Rust’a kıyasla doğrulanabilirlik kademeli olarak daha da iyileşebilir; özellikle de kanıtın zor kısımlarında etkisi büyük olabilir.
Yerleşik özellik olarak en çok eksikliğini hissettiğim şey, “kanıtım üzerinde quickcheck çalıştır” karşılığı bir özellik. Kod elinizdeyken doğru olmayan bir özelliği kanıtlamaya çalışıp kanıtın neden ilerlemediğini anlamaya çalışırken saç baş yolmak kolay. Kanıtın ortasında anlamsız bir duruma ulaşıldığında “buradan bir karşı örnek üret” gibi bir komutun karşı örnek dökmesi iyi olurdu. Kanıtlar büyük ölçüde yol bağımlı ve genelde kolay değil, ama bu araçlar büyüklüğe çok yakın görünüyor. Kodu kanıtlama süreci, o kodun bug barındırabileceği olasılığını da yansıtmalı.
Kanıtlayıcı yanlış bir kanıt üretmez, sadece geçerli bir kanıt çıkarma konusunda başarısız olur. Bu özelliğe sahip makine öğrenmesi uygulamasının çok olmadığını düşünüyorum.
Aslında Rust’ta lock’lar ve referans sayaçları çalışma zamanı yapılarıdır.
Arc, Rust’ın RAII modelini ciddi biçimde bozdu; bu yüzden kapsam bitmeden önce yıkıcının çalışması gereken scoped thread’ler kaldırılmak zorunda kaldı. Küresel referans sayaçlarında döngü ve sızıntı sorunları var ve bu yeniden küresel bir probleme dönüşüyor. Tamamen ortadan kaldırmak zor olabilir, ama arena tarzı kapsamlarla sınırlamanın daha iyi olduğuna inanıyorum. Lock’lar için kanal gibi asimetrik veri yapıları gerekiyor gibi görünüyor. Go’da kanallar gönderici ve alıcı olarak ayrılır; gönderici goroutine’dedefer close(ch)koyabilirsiniz ve panic olsa bile thread’in geri kalanı bittiğinde çalışması garanti edilir. Mutlaka kanal olmak zorunda değil, ama okuma-yazma/üretici-tüketici rollerini ayırmak çıkarımı çok daha kolaylaştırır ve biçimsel analize de yardımcı olur gibi görünüyor.Hoare’ın 1973 civarındaki makalesinden yapılan alıntıyla başlayıp şimdi ikinci yazıya kadar gelmesini seviyorum. Aslında boat’ın yazısının HN başlığında uzun bir yorum yazmış, bu alıntıyı Rust merkezli bir bakış açısına kaydırmanın boat’ın geçmişi düşünüldüğünde anlaşılır olduğunu, ama Hoare eleştirisinin kapsamını yapay biçimde daralttığını söylemiştim.
Şimdi Grayson bu dar parçayı başlangıç noktası alıp Rust’ın birkaç ilginç alanını ve tasarım noktasını tartışmış. Hâlâ kendi yorumumun doğru olduğunu düşünüyorum, ama Grayson’ın yazısından doğan tartışma, çıkış noktası olan yazıya yönelik teknik itirazlarımı dengelemeye yetecek kadar iyiydi.
Ondan sonra basit testlerden daha gelişmiş sağlam olmayan teknikler ortaya çıktıkça, sağlam olmayan yöntemlerin sağlam yöntemlerin önüne geçtiğini düşünüyorum.
Sorunu tespit etmişti ve geriye dönüp bakınca, bir tip sistemiyle paylaşımlı XOR değiştirilebilirliği zorunlu kılma çözümü küçük bir adım gibi görünüyor. O zaman o küçük adımın çözüm olduğunu anlayabilseydik, 50 yıllık muazzam acıyı azaltmış olurduk.
Ama alıntının kendisinin bu bakış açısını güçlendirdiğini sanmıyorum. Hoare’ın daha genel olarak referansların semantik varlığının kendisinden yakınmasını alıp Rust’ın alias’sız değiştirilebilir durum modeline uygulayarak sorunu etrafından dolaşma girişimi olarak görülebilir. Ancak bu, daha büyük bir sorunun yalnızca dar bir parçasını düzeltip tüm sorun ortadan kalkmış demeye daha yakın. Eksik bırakılan kısımlar, özellikle “Variables” bölümünün başı ve ALGOL 68 örneği, Hoare’ın yalnızca değiştirilebilir durumu değil, referans adlı semantik kavramın kendisini eleştirdiği yönüne çok daha güçlü biçimde işaret ediyor. Rust’ın sorunun bir kısmını ehlileştirme girişimini kabul ediyorum, ama hiçbir dilin bu sorunu “düzelttiğini” düşünmüyorum.
Bu yazıya neden bu kadar çok övgü geldiğini pek anlamıyorum. Program analizinin birçok alanını tek bir paragrafla geçiştiriyor gibi. Graydon’ı seviyorum ve bakış açısına saygı duyuyorum, ama bu paragraf fazlasıyla basitleştirilmiş.
GC’li dillerin güçlü yerel akıl yürütme desteğini özellikle sağlamadığı şeklindeki açıklama bir korkuluk safsatası. Pony gibi, tip sisteminde bölgeler bulundurup yine de GC kullanan diller vardı. Ayrıca pointer analizi ve kaçış analizi diye koca alanlar var; benzersizliği çıkarımlar ve iki referansın alias olup olamayacağını belirlerler. Statik tiplerin özü de sınıf ve alan teknikleriyle heap’i birbirine alias olmayan parçalara ayırmaktır. Bu JavaScript meselesi değil; Java/C#/Scala ve sayısız GC dilinde değiştirilebilir durum hakkında yerel akıl yürütme yokmuş gibi davranılmamalı.
Sınıflar ve alanlar, değiştirilebilir durum hakkında tam bir yerel akıl yürütme sağlamaz. Çünkü sınıf/nesne A, sınıf/nesne B’nin değiştirilebilir durumuna bağımlı hâle gelebilir. Java tarzı sınıf kalıtımı da program zamanla evrildikçe kendi başına daha fazla karmaşıklık ekler.
Elbette karşı örnekler var, ama Java, C#, Python gibi ana akım GC’li genel amaçlı dillere bakınca doğru. Nesne yönelimliliğin ilk fikrinin bugünkü aktör modeline yakın olduğu ve sahiplenilmiş veri yapılarını yalnızca mesaj iletimiyle değiştirmeye çalıştığı yorumu yapılabilir. Fakat gerçek dünyadaki nesne yönelimli uygulamalar bu hedefe pek yaklaşmıyor. Java, aynı nesneye yönelik değiştirilebilir referansların birden çok nesnede saklanmasını engellemez. Bu yazı bunu daha iyi açıklıyor: https://without.boats/blog/references-are-like-jumps/
void myMethod(final Map map) { map.remove("key"); int oldSize = map.size(); map.put("key", "val"); int newSize = map.size(); System.out.println(newSize - oldSize); }Düzenleme: Çifte olumsuzlamayı yanlış okumuşum. Tekrar okuyunca hâlâ kafa karıştırıcı. Java’da, JavaScript’ten farklı olarak yerel akıl yürütme olduğu mu kastediliyor?
Graydon’ın yazılarını genelde severim, ama bu yazı, pek çok biçimsel yöntem yazısı gibi alanı bilmeyen okurları yanlış yönlendirebilir. Kurşunu altına çevirmenin yönteminde tek haneli mertebede bir iyileşme olduğunu söyleyip, pratik maliyet etkinliğine ulaşmak için hâlâ 29 haneli mertebede yol kaldığını söylememeye benziyor.
Alias olmaması biçimsel doğrulamayı çok daha kolaylaştırır mı? Evet. Peki bu, gerçek dünyadaki programları pratik ve maliyet etkin biçimde doğrulayabileceğimiz anlamına mı gelir? Kesinlikle hayır. Her gün biçimsel olarak doğrulanan programlar, devreler ve bileşenler var; ama bunlar istisna niteliğinde, görece çok küçük ve özel olarak dikkatli bir yöntemle geliştiriliyor. Yerel akıl yürütmeye yardımcı olan özellikler önemlidir, fakat ana akım yazılımların doğruluğunu sağlam bir yöntemle garanti etme biçiminde kayda değer bir değişiklik yaratmaz.
Heap’i, pointer’ı, integer’ı olmayan; yalnızca boolean değişkenleri bulunan ve döngüleri ikiden fazla dönemeyen, Turing-tam olmaktan uzak bir dildeki programlar bile TQBF’ye indirgenebildiği için pratikte doğrulanamaz. Bazı özellikler, örneğin bellek güvenliği için bu mümkün olabilir; ama yazılımın ihtiyaç duyduğu şeyler için yeterli değildir. 1970–90’larda, en kötü durum karmaşıklığı yönetilemez olsa bile dilin yerel garantileri ve yapısının bizi en kötü durumdan uzaklaştıracağı umudu vardı; ancak sonrasında bunun böyle olmadığı kanıtlandı. İnsanların gerçekten yazdığı programların en kötü durumdan iyi sezgiseller çıkaracak kadar uzak olduğu umudu da artık pek geçerli görünmüyor.
Bununla ilgili bir sunum var: https://pron.github.io/posts/correctness-and-complexity
Temel sonuç şu: Doğrulamak isteyeceğiniz ilginç özelliklerin çoğu bileşmez. P1...Pn bileşenlerinin her biri için bir özelliği kanıtlasanız bile, P1 ○ ... ○ Pn için o özelliği kanıtlamanın maliyeti yalnızca n’e göre süper-polinom biçimde artmakla kalmaz, her bir bileşenin boyutuna göre de süper-polinom artar. Yani parçalamadığınız zamanki kadar zordur; doğruluk ayrıştırılamaz. Bu yüzden “epey çok şeyi doğrulayabiliriz” ile “doğrulanabilenler denizde bir damladır” aynı anda doğrudur ve biçimsel yöntem tartışmalarında bu uçurum sık sık atlanır.
Tamamen yanlış değil, ama tamamen doğru da değil. Bu konuyla ilgilenen pek çok kişinin, yüzlerce tekrar içinde bunu gösterme fırsatı bolca olmuşken görüşünün hiç evrilmemiş olması şaşırtıcı. Bu tutum hastalıklı bir kapalılık gibi duyuluyor ve tartışmaya katılan herkesin zamanını boşa harcatıyor.
Bu tekrar tekrar oluyor. Sağlam yöntemlerde önemli iyileştirmeler olurken bile, sağlam olmayan yöntemler pratikte daha doğru yazılıma doğru çok daha büyük ilerleme sağladı. Çok yakın tarihli bir örnek olarak https://antithesis.com var. Elbette belirli durumlarda sağlam teknikler daha güçlü ve pratik olabilir; bu karmaşık bir konu.
unsafekullanımını doğru yapıp yapmadığını doğrulayabilir hâle gelmeyi beklemek makul. Bu tek başına bile gerçekten faydalı.F* yazısına da az önce ilgili bir yorum bıraktım. Söz dizimine bakınca öznel olarak Rust yerine F*/F#’ı tercih ediyorum, ancak geliştirmekte olduğum gösteri kontrol yazılımında Ada/SPARK2014 kullanmaya karar verdim.
Rust’ın Ada/SPARK2014 ile aynı tür insanları çekebilmesi için C, Common Lisp, Prolog, Fortran, COBOL gibi mevcut dillerde olduğu gibi resmî yayımlanmış bir standarda ihtiyacı var. AdaCore ile Ferrous Systems, Ada/SPARK2014’tekine benzer şekilde Rust için biçimsel doğrulama araçları sunmak üzere iş birliği yaparken Rust da bu alana giriyor; ancak henüz yayımlanmış bir standardı yok ve Ada ile SPARK2014’ün mirası çok büyük.
Referans sayımını, kesin biçimde çevrimsiz verilere uygulandığında ya da döngüsel sızıntıları göze alabildiğinizde çalışan, bir tür hemen çalıştırılan optimize GC olarak görebilmek ilginç. Python, yazıda anlatılan referans sayımı + izleme karması yaklaşımı kullanır; izleme toplayıcısını yalnızca her N istekte bir çalışacak şekilde zorlayan üretim dağıtımları da gördüm
Perl saf referans sayımı kullanır ama zayıf referanslara sahip olduğu için, döngüsel yapının hangi kısmının referansını tuttuğunuza dikkat etme pahasına veriyi referans sayımı açısından çevrimsiz hâle getirebilirsiniz. Koka teoride referans sayımı kullanır, ama pratikte bunu mümkün olduğunca derleme zamanına taşımaya çalışır;
y = x + 1içindexiçin yalnızca tek referans olduğu ve sonrasında kullanılmadığı garanti edilebiliyorsa,yiçin aynı depolamayı yeniden kullanıp yerinde değişiklik yapabilirNim, ORC sunar; bu, otomatik referans sayımına Bacon+Rajan’ın Recycler algoritmasının uygulanmasının eklenmiş hâlidir. Bu algoritma, referans sayımı tabanlı sistemlerde yalnızca döngüleri toplamak üzere tasarlandığından oldukça hızlıdır. Rust tarafına dönersek, stop-the-world Recycler uygulaması burada: https://github.com/fitzgen/bacon-rajan-cc ve bu fork’ta bacon-rajan-ccc crate’i olarak yayımlanıyor: https://github.com/mbartlett21/bacon-rajan-cc README’deki Alternative bölümünde aynı alandaki başka deneylere bağlantılar var. Recycler makalesini bulmak zorsa, kopyalarını https://trout.me.uk/gc/ altında topladım; benzer zevklere sahipseniz https://trout.me.uk/lisp/ altındaki makalelerden de keyif alabilirsiniz
Programların biçimsel doğrulaması konusunda sabırsızlık hissediyorum. Bir programın belirtimi doğru uyguladığını kanıtlamak teorik olarak ilginç, ama pratikte pek işe yaramıyor
Doğru belirtim yazmak, doğru programlama kadar zor olduğundan, zor problem çözülmüyor; yalnızca başka yere taşınıyor. Biçimsel yöntemlerin pratik kullanım alanları var, ama bunlara nadiren rastlanıyor
Bunları yapabildiğinizde önkoşul olarak zorunlu kılabilirsiniz. Örneğin bir fonksiyona dizi geçmeden önce o dizinin önceden sıralanmış olduğunu göstermeniz gerekmesi gibi
15 Mayıs 2024’te yazılmıştı; o gün Rust 1.0’ın 9. yıl dönümüydü
Bağlantısı verilen Boats yazısını okudum ve harikaydı. Hoare’ın 50 yıl önceki alıntısının hâlâ ilgili olması ve ifadesinin de çok iyi olması şaşırtıcıydı
Daha basit bir yaklaşımla derleme zamanı type guard benzeri şeyler kullanabilmek isterdim. trait bound’lar çoğalınca tip düzeyi programları okumak zorlaşıyor
Örneğin
Where <<::Output as G>::Output as H>::Output: HList + Zya datype Output = <<::Output as G>::Output as H>::Output;gibi. BunaCons>>>ekliyorsunuz ve TypeNum’dakiU8gibi sayıların bile aslında kendi içindeCons>>iç içe geçmesi olduğunu fark ediyorsunuz. Bu alanda ilerleme kaydedip istenen doğrulamayı yaptırmak mümkün, ama hata mesajları insan geliştiricilerin kod yazma biçiminden çok farklılaşabiliyor ve uygulaması da çok sancılı oluyorGeliştirici deneyiminin şaşırtıcı olmasının nedeni bunun “sadece bir fonksiyon” değil, belirli generic’ler ve ilişkili tiplerin bir birleşimi olması. Çalışma zamanı tarzı kontroller kullanıp bunları derleme zamanında çalıştırmak istiyorum, ama bunu yapmak için epey farklı kod yazmam gerekti. Sonuçta tip düzeyi derleme zamanı Rust’ını daha basit, fonksiyonel ve okunabilir kılmak, bu tür biçimsel analiz projelerinin bakımcılar ve kullanıcılar için iyi bir deneyim sunmasının yolu olabilir. Özetle
comptimeRust istiyorum. AyrıcaPin<&mut Self>tabanlıFuture’ın şimdiden yerleşip yerleşmediğini de merak ediyorum.async/awaitiçin farklı iç uygulamaları denemek isterdim, ama nereden başlayacağımı bilmiyorum