Biçimsel yöntemler ve programlamanın geleceği
(blog.janestreet.com)- Biçimsel yöntemler, yazılımın amaçlanan özellikleri sağladığını kanıtlayan araçlardır ve ajan destekli kodlamanın yaygınlaşmasıyla maliyet-fayda değerlendirmesi değişiyor
- Jane Street geçmişte, bazı özel durumlar dışında biçimsel yöntemlerin maliyetine göre değerinin düşük olduğunu düşünüyordu; ancak şimdi özel bir ekip kuruyor
- seL4'ün 8.700 satırlık C kodunu doğrulamak için 25 kişi-yılı gerekti ve her bir kod satırı için yaklaşık 23 satır kanıt ile yarım kişi-günlük doğrulama gerekti
- Ajanların ürettiği kod ile yayımlanabilir kalite arasında fark var; bu nedenle doğrulama darboğazını azaltan ve ajanlara güçlü geri bildirim veren bir araç olarak biçimsel yöntemler önem kazanıyor
- Jane Street, dili derinlemesine denetleyebildiği ve hazır bir programcı topluluğuna sahip olduğu için OxCaml ile kanıt odaklı teknikleri birlikte geliştirmek için alan olduğunu düşünüyor
Biçimsel yöntemler ve programlamanın geleceği
- Jane Street son 25 yıldır kurumsal düzeyde biçimsel yöntemlerle ilgilenmediğini söylüyordu, ancak artık bu tutumu sürdürmüyor
- Daha iyi ve daha güvenilir kod yazmaya yarayan araçların gücünü uzun zamandır önemsiyor ve tip sistemlerini büyük fayda sağlayan hafif biçimsel yöntemler olarak görüyor
- Özel durumlar, özellikle de donanım sentezi dışında, biçimsel yöntemlerin maliyetinin çok yüksek olduğu ve çoğu yazılım için uygun olmadığı değerlendirmesini yapıyordu
- seL4 biçimsel olarak doğrulanmış bir mikrokernel ve önemli bir başarıydı, ancak 8.700 satırlık C kodunu doğrulamak için 25 kişi-yılı gerekti
- Her bir kod satırı için yaklaşık 23 satır kanıt gerekiyordu ve bir satırın doğrulanması için yaklaşık yarım kişi-gün gerekiyordu
- Güvenliğin kritik olduğu mikrokerneller gibi, riskin yüksek ve belirtimin görece net olduğu durumlarda bu yaklaşım değerli olabilir
- Bu, çoğu yazılım için uygun değildi ve Jane Street'in en önemli yazılımları için de uygun görünmüyordu
- Ajan destekli kodlamanın ortaya çıkışı bu değerlendirmeyi değiştirdi ve biçimsel yöntemlerin potansiyeline dair kuşkular beklentiye dönüştü
- Jane Street bir biçimsel yöntemler ekibi kuruyor ve bunu gelişmiş tip sistemleri kadar geniş ölçekte faydalı bir yazılım geliştirme aracına dönüştürmeyi umuyor
Neden fikrimiz değişti?
- Ajan destekli kodlama, biçimsel yöntemlerin mevcut maliyet-fayda dengesini çeşitli şekillerde sarsıyor
- Bu, ajanların kendi başlarına rastgele zor kanıtlar kurabildiği anlamına gelmiyor; ancak modeller büyük yardım sağlıyor ve daha fazla kişinin bu araçları verimli kullanmasını mümkün kılıyor
- Biçimsel yöntemleri kullanmak eskisine göre daha kolay hale geldikçe, geçmişteki maliyet-etki hesabını yeniden değerlendirmek anlamlı hale geliyor
-
Doğrulama darboğazı daha önemli hale geliyor
- Modeller giderek daha faydalı kod yazıyor, ancak modelin ürettiği kod ile gerçekten yayımlanabilir kod arasında büyük fark var
- Modeller, verilen hedefe ulaşmada şaşırtıcı derecede başarılı olsa da bu süreçte kod tabanının kalitesini koruma veya iyileştirme konusunda yeterince güçlü değil
- Ajanların yazdığı kod gelişiyor, ancak aşırı karmaşık olma, garip hatalar ve sınır durumları barındırma ve kod tabanının temel değişmezlerine uymama eğilimi taşıyor
- İnsanlar, ajanların ürettiği kodun yeterli kalitede olup olmadığını doğrulamak için çok zaman harcamak zorunda kalıyor
- Biçimsel yöntemler bu doğrulama yükünü azaltabilir ve inceleme sürecini daha verimli hale getirebilir
-
Ajanlar geri bildirimle güçleniyor
- Ajanlar hem pekiştirmeli öğrenmeyle eğitilirken hem de kodlama için kullanılırken geri bildirimden fayda sağlıyor
- Biçimsel yöntemler, ajanların zor problemleri çözme becerisini artırabilecek güçlü bir geri bildirim biçimi sunuyor
- Testler de çok değerli ve özellik tabanlı test ile fuzzing kullanıldığında daha da iyi sonuç alınabilir
- Ancak yalnızca test yeterli değil; programın keşfedebileceği durum uzayını kapsama konusunda doğal sınırlar var
- OxCaml programlama deneyiminde ajanlar, tip sisteminin sağladığı evrensel garantilerden büyük fayda görüyor
- Tip sistemi veri yarışlarını engelleyebiliyorsa veri yarışları ortadan kaldırılabilir
- Tipleri iyi kurgulayarak cross-site scripting açıklarını imkânsız hale getirmek, yalnızca basit testlerle elde edilmesi zor bir şekilde bu açıkları ortadan kaldırabilir
- Tipler, ajanlarla birlikte programlama yaparken doğrulama darboğazını hafifletir ve daha iyi geri bildirim sağlar
- Daha güçlü kanıt tekniklerinin kullanılmasıyla ek ilerleme alanı olabilir
Neden burada yapılıyor?
- Tüm dünya, ajanların programlamanın geleceği için ne anlama geldiğini düşünüyor ve biçimsel yöntemlerle ajanları birleştirmeye çalışan birçok startup var
- Jane Street kullandığı dili derinlemesine denetleyebildiği için dili kanıt odaklı tekniklere daha uygun olacak şekilde ayarlayabilir
- Olası yönler çeşitli
- Özelliklerin modüler belirtimleri tip sistemine entegre edilebilir
- Sahiplik ve değiştirilebilirlik gibi unsurlar için tip düzeyinde kısıtlar eklenerek belirli kanıtlar kolaylaştırılabilir
- Kanıt teknikleri doğrudan dile yerleştirilebilir
-
Hazır bir programcı topluluğu
- Jane Street'te bu tür teknikleri benimsemeye hazır bir programcı topluluğu var
- Programlama dilleriyle uğraşanlar için, daha iyi programlama fikirleri geliştirmekten daha zor olan şey çoğu zaman bu fikirleri gerçek işte kullanılabilir hale getirmektir
- Jane Street'te kullanıcıların, vaat edilen yeni ve alışılmadık tip sistemi özelliklerinin yeterince hızlı gelmemesinden şikâyet ettiği sık görülür
- Bu tekniklerden yararlanabilecek arka plana sahip çok sayıda insan var ve doğru sonuçlar ile yüksek kaliteli yazılım üretmeye yönelik ilgi zaten yerleşmiş durumda
- Etkin ve beklentisi yüksek bir kullanıcı tabanı, kısa vadeli iyileştirmeler ile uzun vadeli vizyonu aynı anda deneme özgürlüğü veriyor
- Kısa vadeli iyileştirmeler görece hızlı biçimde etki yaratabilir
- Uzun vadeli vizyon ise birkaç yıla yayılan daha iddialı hedeflere dönüşebilir
- Kısa vadeli denemelerden öğrenerek uzun vadeli hedeflere doğru inşa edilebilir
-
Dış araçlarla ilişki
- Dış dünyadaki çalışmaları görmezden gelmiyor ve çeşitli programlama dili topluluklarının çalışmalarından umut ve ilham alıyor
- İlgili araçlar arasında Lean, Dafny, Rocq, Agda, Iris bulunuyor
- OxCaml'i bazı araçlarla entegre ederek mevcut güçlü altyapıdan yararlanmanın yollarını arıyor
- Ayrıca dili ve kanıt tekniklerini aynı anda ele alındığında ortaya çıkabilecek benzersiz avantajlar da olduğuna inanıyor
Katılım çağrısı
- Jane Street, London ve New York için biçimsel yöntemlerle ilgili pozisyonlara alım yapıyor
- Bu pozisyonlar için mülakatlar ve ekip oluşturma süreci şu anda erken aşamada
- Yapılacak çok iş var ve ekibe katılacak kişiler aranıyor
Ek notlar
- Modeller, karmaşık kanıtları ele alırken hâlâ insan yardımı ve yönlendirmesine ihtiyaç duyuyor
- İnsan programcılar, sistemin neden çalıştığına ve bunun yüksek seviyede nasıl kanıtlanacağına dair fikirlere sahip olabilir
- Çoğu programcı, belirli bir kanıt sistemini tatmin edecek şekilde kanıt fikrini nasıl kodlayacağını bilmiyor
- Modeller, kanıt yazmanın teknik ayrıntılarındaki çok sayıda tekrarlı işi otomatikleştirebilir ve uzmanlık sağlayabilir
Obj.magicgibi kaçış yolları tip düzeyindeki kısıtların aşılmasına neden olabilir- Çoğu kodda bu tür istisnalar izlenip yasaklanırsa evrensel garantilere çok yakın bir durum elde edilebilir
- Biçimsel yöntemler, bu tür kaçış yollarının kullanımının neden gerçekten güvenli olduğunu açık hale getirebilir
1 yorum
Hacker News görüşleri
Onlarca yıl önce doğruluk ispatı işi yaptım ve o zamanki sistem, sonraki birçok sistemden daha fazla ispat otomasyonuna sahipti
Kolay kısımları ilk SAT çözücüsü olan Oppen-Nelson sadeleştiricisi hallediyordu, zor kısımları ise sezgisel yöntemler ve önceki yardımcı lemmaları kullanan Boyer-Moore ispatlayıcısı üstleniyordu. İnsanın zor görevi, ispatlayıcının denemesi ve sonraki ispatlarda kullanması için yardımcı lemma önermekti
Sonraki sistemlerde otomasyon azalmış gibi göründü ve biçimsel yöntemlerin raydan çıkma nedeni bence pratiğe kıyasla biçimciliğe fazla kapılmalarıydı. Ticari projelerde hatasız kod isteyen biri olarak, akademik tarz projelerin makaleye uygun kısa gösterim ve az sayıda durum analizini tercih eden matematikçi önyargısına kapıldığını hissettim
Gerçekte çok fazla otomatik angarya ve daha az içgörü gerekmesi lazım. Zeki insanlar kâğıt kalem ispatların laf kalabalığından kaçınmak için modal mantık, zamansal mantık gibi yeni mantıklar üretip durdu ama bunun pek faydası olmadı. Bu alanın temel gerçeği, çoğu teoremin oldukça sıradan olduğudur
Jane Street ekibinin de söylediği gibi, dili kontrol edebilmek büyük bir avantaj. Doğrulama ifadeleri programlama dilinin içine entegre edilmeli; yorumlarda, başka bir sözdiziminde ya da ayrı dosyalara gömülü olduklarında gereksiz iş artıyor. Jane Street'in bu yönü zorlaması iyi görünüyor
Bu işi 40 yılı aşkın süre önce, fazla erken yaptım; o zamanlar Boyer-Moore ispatlayıcısıyla sayı teorisini sıfırdan kurmak yaklaşık 45 dakika hesaplama süresi alıyordu ama artık 1 saniyeden kısa sürüyor
https://archive.org/details/manualzilla-id-5928072/page/n3/m...
Mantık, bilgisayar bilimi ve yazılım mühendisliğinde fizik, makine mühendisliği ve inşaat mühendisliğindeki kalkülüsle benzer bir konumdadır. LTL ya da daha yeni ayırma mantığı gibi şeyler muazzam atılımlardı
Epey popüler olan TLA+ bunun kanıtı ve model denetimi çok pratiktir. Şu anda ilginç olan nokta, daha ağır biçimsel yöntemlerin, özellikle de teorem ispatının, genel sistem yazılımında bile kullanılabilecek kadar ucuzlayıp ucuzlamayacağıdır
Bir fonksiyon için biçimsel belirtim yazıp bunu SAT/SMT, teorem ispatlayıcı ve LLM hibritiyle sentezleyerek doğruluğunu ispatlatma yöntemi çok yakında standart hâline gelebilir
On the Unusual Effectiveness of Logic in Computer Science: https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf
From Philosophical to Industrial Logics: https://www.cs.rice.edu/~vardi/papers/icla09.pdf
Kaygı verici olan, çözmesi zor bir matematiğin ortaya çıkması ve bunu koruyan küçük bir müridler topluluğunun oluşması. Birbirinden farklı, anlaşılması güç gösterimler birbiriyle uyumlu olmayacak ve birini anlamak diğerini anlamada pek yardımcı olmayabilecek. Çoğu kişi yalnızca düzgün biçimde doğrulanamayan İngilizce cümleler yazacak
Daha kötüsü, makinelere kendi cümlelerini biçimselleştirtip, o biçimciliği ya da ispatı anlamadan doğrulama tiyatrosuna katılabilir ve her şey patladığında şaşırmış gibi davranabiliriz
Tip sisteminin hızlıca ele alamadığı kısımlara bu yetenekleri entegre etmeye yönelik çalışmalar yavaş ilerliyor; bu yüzden bu yoldan daha önce geçmiş kişilerin bakış açısı ilgimi çekiyor
Güzel. Son birkaç ayda Scala 3'te ifade gücü yüksek tipler kullanarak tiplerin giderek daha fazla derleme zamanı ispatı taşımasını sağlamaya geçtim. Makro kullanmıyorum ama bazıları işe yarayabilir
Bu yaklaşım yalnızca ajan tarzı testlerin yayılma sorununu azaltmaya yardımcı olmuyor, aynı zamanda ajanın düşük kaliteli çalışma biçimlerine düşmesini de engelliyor gibi görünüyor. Özellikle de ajanın makul biçimde genelleştirmesi gereken durumlarda her şey için yeni bir tekil tip yaratmaya çalıştığı isim biriktirme eğilimini engelliyor
İyi kalitede ajan kodlamasını hızlandıracak tarafın, güçlü tip sistemine sahip diller de dâhil olmak üzere, biçimsel yöntemlere benzeyen araçlar olduğunu düşünüyorum
Burada ifade gücü yüksek tiplerden kastım, ekip zaten tip düzeyi programlamaya aşina değilse genel bir kod tabanına koymak istemeyeceğiniz teknikler. Yani yüksek dereceli kind'ların ve tip fonksiyonlarının tuhaf şeyler değil, temel yapı taşları olduğu bir ekip olmalı
Ajanlar bilgi açısından çoğu geliştiriciden daha iyi “matematik” yapıyor ve çoğu zaman kategori teorisine fazla dalmış geliştiricilerden bile daha iyiler. Üstelik konuşma konusunda “sonsuz” sabra sahip olduklarını varsayarsanız eğitim vermede de oldukça iyiler
Kişisel olarak Codex'e birkaç hobi ispatını Lean tarzına dönüştürttüm ve bu çok kolaydı. %100 “doğru” olduğunu söylemiyorum; daha sıkı doğrulamak için Lean 4'ü daha fazla öğrenmem gerekir ama görünüşe göre klasik ispat tuzaklarını da temel düzeyde kontrol ediyor. Biçimsel yöntemlerin geleceği beni çok heyecanlandırıyor
Gen AI çok fazla kod ürettiği için, insanların değerini doğrulama tarafına kaydırmamız gerektiği söyleniyor gibi görünüyor. Programlamanın gerçekten ne olduğunu ara sıra düşünüyorum
Ana dili İngilizce olmayan biri için programlamayı öğrenmek başlı başına büyük bir meydan okuma. Çevrilmemiş İngilizce belgeleri anlamak için makine çevirisine güvenmek zorundayım ve kendi dilimdeki kaynaklar 5-6 yıl kadar geriden geliyor
Artık yapay zekanın ürettiği on binlerce satır kodu code review'dan geçirmek imkansız hale geldiği için, matematiksel ispat gibi mutlak kurallar koyalım yönünde tartışmalar görüyorum. Bu yazıyı okuyunca Rust'ın borrow checker'ı aklıma geldi. Gerçekten Rust'ı birkaç kez kullandığınızda, insanların borrow checker'dan kaçmak için hileli yollar denemeye yöneldiğini ve bunun kötü alışkanlıklara dönüştüğünü görüyorsunuz
Matematiksel katılık aşırıya kaçarsa insanlar dolambaçlı yollar aramaya başlıyor. Benim gibi eğitimi sınırlı programcılar bunu yapmaya özellikle daha yatkın
Bu tür girişimler sonunda yalnızca belirli biçimselleştirilmiş cevaplara yönelik kod yazılmasıyla sonuçlanacak gibi geliyor. Bu kadar standartlaşınca insan ihtiyaçlarına yanıt verip veremeyeceğinden emin değilim
Bu tür savunmacı programlama girişimleri fena değil ama ben, kendi ifademle, saldırgan programlama yapmak istiyorum. Risk alıp hızlıca düzeltmek ve dağıtmak, zamanla yeterince iyi hale geleceğine inanmak gibi bir yaklaşım bu
Elbette Jane Street gibi doğruluğun önemli olduğu ve iş kapsamının iyi tanımlandığı yerleşik sektörlerde bu yazıdaki yaklaşım mantıklı. Çünkü piyasa taleplerini uygun şekilde modelleyecek kadar veri var
Ama para kazanmak için altın madeni arar gibi sürekli yer değiştiren benim gibi sosyal kaybedenler için bu tür metodolojiler lüks gibi görünüyor. Olgun modellemeye sahip mevcut işler, yüksek eğitimli uzmanların sürekli optimizasyonunu gerektiriyor ve gerçekte bu talebi karşılamanın mümkün olmadığını biliyorum. Bu yüzden modellemenin yapılandırılmadığı yerleri arıyorum ama oralarda da bu yaklaşımın işe yarayıp yaramayacağını bilmiyorum
Orada “sonra düzeltiriz” diye bir şey yok. Neyin yanlış gittiğini anlayana kadar çoktan milyarlar kaybetmiş olabilirsiniz
Bu yüzden saldırgan yaklaşım çekirdek olmayan alanlarda işe yarayabilir
Ayrıca, savunmacı yaklaşım zaten birçok yerde kullanılıyor. Python, Java vb. dillerde garbage collector var ve bu da kodun amaçlandığı şekilde çalıştığının bir tür doğrulaması sayılabilir
Biçimsel doğrulamanın ne zaman görünür olmaya başlayacağını merak ediyordum; uygulama ayrıntılarıyla uğraşma aşamasından, problemi bilimsel ve matematiksel olarak tanımlama aşamasına geçmek doğal görünüyor
Gen AI yüzünden savunmacı programlamanın maliyeti ciddi biçimde düştü, insan doğrulamasının maliyeti ise ciddi biçimde arttı. Buna karşılık biçimsel yöntemler doğrulamayı ucuzlatıyor ama spesifikasyon, tipler, ispatlar yazmak ve uygulamayı sert bir kalıba uydurmak gibi büyük bir uygulama yükü getiriyor
Fakat Gen AI bu zahmetli işleri otomatikleştirebilir. İkisi birbirine biçilmiş kaftan
Bir miktar çaba gerektirir ama sürekli çeviri ek yükünü ortadan kaldırmak muazzam fayda sağlar
Ama birinin kendine “sosyal kaybeden” demesinin ya da kariyerinde bu tür pratikleri izlemediğini söylemesinin bu tartışmayla nasıl ilişkili olduğunu pek anlayamadım
Son zamanlarda buna yakın fikirlerle oynuyorum ve beni şaşırtan şey, en ileri modellerin, özellikle ChatGPT-5.5'in, Roqc'ta yani eski adıyla Coq ispat yardımcısında bazı manuel ispatları ne kadar iyi tamamlayabildiği oldu
İspatlar her zaman zarif değil ama ChatGPT, bende az da olsa olan ispat yardımcısı deneyimi ve ispatlanan lemma alanında oldukça geniş bir alan bilgisiyle bile, benim çok daha uzun sürede yapacağım işleri çoğu zaman birkaç dakika ve 10-100 deneme içinde tamamlıyor
Bu kısa yazının bağlamında bunun ilginç olmasının nedeni, bazı biçimsel yöntem araçlarının çalışma varsayımlarını sarsması. Frama-C, Ada/SPARK gibi araçlar, CVC5 ve Z3 gibi araçların otomatik olarak çözebileceği proof obligation'lar üretmeye odaklanıyor; bu başarısız olursa Roqc'ta manuel ispat gibi oldukça acı verici bir alternatife geçiliyor
Yaygın akış, bir yükümlülüğün “zor” olduğunu, yani otomatik çözülemediğini fark ettikten sonra, kodun yükümlülük ürettiği noktada görünen lemma ve assertion kümesini yeniden düzenleyerek onu “kolay” hale getirmek ya da hatta kodu değiştirmek oluyor
Roqc ispatlarının iki kat pahalı olduğu bir dünyada bu mantıklı. Çünkü insanların yazması zor ve kod ile çevresindeki ispatlar değiştiğinde bakım oynaklığı da yüksek
Ama eğer Roqc ispatları “AI döngü içinde otomatik çözüyor” haline gelirse, bu maliyet farkı ortadan kalkar. O zaman ispatları da kod gibi yazabilir, insan tarafından okunabilir açıklığı birinci öncelik yapıp derleyici veya ispatlayıcı optimizasyonunu çok daha geri plana atabiliriz. Bunun sonuçlarını henüz tam sindirebilmiş değilim ama oldukça ilginç
İspatla hiç uğraşmadım ama “değişiklikten sonra bu test başarısız oldu” dediğinizde, AI'ın benim niyetim olan eski testi ve yeni testi birlikte geçecek şekilde kodu düzeltmek yerine testin kendisini değiştirdiğini bazen gördüm
Devamını merakla bekliyorum
Biçimsel belirtimlerle ilgili bir şey okuduğumda, her seferinde bu bana “aynı testleri başka bir şekilde yazmak” gibi görünüyor; daha kötüsü, “aynı implementasyonu başka bir şekilde yazmak” gibi görünüyor
İki kez yazmak hataları yakalamaya yardımcı olabilir, ama biçimsel belirtimlerin de testler ya da implementasyonla tamamen aynı türden hatalara sahip olabildiği durumda bunun özel yanı tam olarak ne, pek emin değilim
Temel sorun şu gibi geliyor: bir programın bir şeyi yaptığını biçimsel olarak kanıtlamak için, o “şeyi” çok somut biçimde tanımlamak gerekiyor. Bu da fiilen testi ya da implementasyonu yeniden yazmak gibi oluyor
Bu konuya yıllardır aralıklı olarak bakıyorum ve sürekli bir şeyi kaçırıyormuşum hissi var, ama onun ne olduğunu bilmiyorum. Bunu biri açıklayabilir mi
Testlerin kusuru, yalnızca sorun çıkarabileceğini düşündüğünüz davranışları test edebilmenizdir. Yanlış gidebileceğini bilmediğiniz davranışları da önceden düzeltmek için araç kutusunda daha sıra dışı araçlara ihtiyaç vardır. Fuzz testi bu yönde bir başlangıçtır ve biçimsel doğrulama da bir başka başlangıçtır
Elbette bu araçların kalitesi, istenen davranışlara izin verip istenmeyenleri yasaklayan kapsamlı bir biçimsel modeli ne kadar iyi yazdığınıza bağlıdır; ve birçok alanda biz hâlâ şaşırtıcı derecede bu noktadan uzağız
Örneğin birim testinde “foo('abc') sondaki boşlukları olmayan bir string döndürür” diye yazabilirsiniz
Ama biçimsel yöntemlerle “rastgele bir girdi x için foo(x) sondaki boşlukları olmayan bir string döndürür”ü kanıtlayabilirsiniz
Basit bir örnek, ama “rastgele bir program P için compile(P), P ile aynı davranışı sergiler” gibi daha karmaşık şeyleri de hayal edebilirsiniz
Tabii “aynı davranış”ın ne olduğunu tanımlamanız gerekir
Tasarımın özelliklerini tanımlarsınız, sonra araç tasarımı çeşitli şekillerde test ederek bu özellikleri ihlal edip edemeyeceğini kontrol eder
Örneğin trafik ışıklarını kontrol eden bir sistemde, kesişen şeritlerin aynı anda ya da belli bir süre aralığı içinde ikisinin birden yeşil olamayacağı özelliğini tanımlayabilirsiniz
Araç bunu kapsamlı arama ile kontrol eder ve ihlale yol açan kod izini gösterebilir
Statik olarak kanıtlanan bir tip sistemi, her bileşenin diğer tüm bileşenlerle önceden uyumlu olacak şekilde kontrol edilmesini sağlar. Sadece “bu test geçiyor” değil, bir araya geldiklerinde “bu testlerin tümü makul ve tutarlı bir bütün oluşturuyor”u garanti eder ve tutarsız bir modelin koda geçirilmesini engeller
Bu, Rust’ın
matchyapısının mümkün olan tüm dalları eksiksiz kapsamasını zorunlu kılmasının, tüm kod tabanı ölçeğine genişletilmiş hâli gibi düşünülebilirTemel mantık ya da teori hataları yaparsanız bunu yakalayamayacağı doğrudur. Ama örneğin Haskell tip sistemi, geçici fonksiyonel testler ve özellik testlerinin birleşiminden çok daha sağlam olduğuna şaşırabilirsiniz. Bunların toplamı da güçlü bir sistem sayılır, ama biçimsel olarak kanıtlanmış kriptografi çok daha yüksek bir çıtadır
Özellikle eşzamanlılık, dağıtık ve çok iş parçacıklı durumlarda değeri büyüktür. Race condition ve deadlock’ları test etmek ve üzerlerinde akıl yürütmek çok zordur; “A, B, C olayları A, C, B sırasıyla gerçekleşebilir mi?” gibi sorular buna örnektir
Bu alanın olgunlaşması muhtemelen kabaca şöyle ilerleyecek. Birincisi, LLM’ler başlangıçta ancak “ikinci kez deneme” türü sonradan doğrulama düzeyinde kalsalar bile, biçimsel yöntemleri öğrenmeyi ve kullanmayı çok daha hızlandıracak
İkincisi, “implementasyon kodu değişti; bu modelin bozulduğu anlamına mı geliyor?” sorusunu LLM’in kontrol ettiği otomasyona geçilecek. Hâlâ belirleyici olmayacaktır, ama nadiren değişen bir şeyi insanların gözden geçirmek zorunda kalmasından büyük olasılıkla daha iyi olacaktır
Üçüncüsü, asıl sıçrama “yalnızca biçimsel belirtimi yaz, implementasyonu üret” diyen araçları bir sonraki seviyeye taşımakta olacak. Böyle kod üretimi projeleri zaten var, ama çoğu şirketin istediği olgunluk düzeyine henüz tam ulaşmış değil. LLM araçları, bunlardan birini ihtiyaca uyarlamak için gereken 1-2 yıllık el emeğini hızlandırabilse nasıl olurdu
Kleppmann’ın önceki yazısı https://martin.kleppmann.com/2025/12/08/ai-formal-verificati... da bakmaya değer; ayrıca tip sistemine ya da linter’a eklenebilecek bir şey varsa, elbette bunu yapmak gerekip gerekmediği tartılmalı
Umarım daha kullanışlı bir yaklaşım ortaya çıkar. Yazıda geçen araçlar arasında dafny ve iris endüstriyel kullanıma en yakın olanlar gibi görünüyor. Amazon S3’ün de içeride TLA kullandığı bir geçmişi olduğunu biliyorum
Ama bu alanın TypeScript benzeri bir şeyi — mevcut araçlara doğal biçimde giren, sıfır maliyetli soyutlamalar gibi çalışan ve insanların gerçekten önceki yöntemlere kıyasla tercih ettiği bir şeyi — henüz gördüğümü sanmıyorum
Özel linter kullanmak da hâlâ oldukça kötü. golangci-lint acı veren bir codebase, semgrep’i kullanmadım ama kural motoru göz korkutucu görünüyordu. Hoşuma giden bir AST API’si de henüz kullanmış değilim
Tümdengelimsel akıl yürütmeye, yani “biçimsel yöntemler”e yönelik bu övgüler, her zaman onun temel sınırlamasını atlıyor. Sorun, aksiyomların ve tanımların hedef alanla ne kadar iyi örtüştüğü
Bu, “Teoride teori ile pratik arasında fark yoktur. Pratikte ise…” sözü gibi. Jane Street’in, kodun amacının belirleyici algoritmaları uygulamak olduğu ve bu yüzden eşlemenin 1:1 olduğu büyük bir kod tabanını sürdüreceğini varsayıyorum. Pek çok geliştirici böyle alanlarda çalışıyor, ama milyonlarcası çalışmıyor. Çoğu UI, çoğu keşif odaklı iş vb. böyle değil
Biçimsel yöntemlerin yanında, mantıksal ya da matematiksel olmayan ama kabul ölçütlerini yüksek çözünürlükte tanımlamaya çalışan bir akım da var. Bu akım en azından eşleme sorunuyla boğuşuyor, ama haritanın bölge olmadığı çoğu yerde bunu çözemiyor
Google arama sonuç sayfası son derece gelişmiş bir iç optimizasyon çerçevesine sahip, ama gerçekten optimum noktaya ulaştı mı? Belirsiz bir fikri yakalamak için aceleyle yapılmış bir prototip bunu daha iyi gösterebilir miydi? Bu tür sorular en iyi, sistemin içinden değil, o sistemin hizmet ettiği dışarıya bakılarak yanıtlanabilir
Mantık devreleri, yoğun biçimsel doğrulama içeren CPU bileşenleri, çekirdekler, protokoller, ayrıştırıcılar, derleyiciler, kriptografi, güvenlik çerçeveleri, eşzamanlılık temel taşları vb. doğrulamadan büyük fayda sağlar
Daha fazlasını öğrenmek için Hillel Wayne’in yazısı iyi bir başlangıç noktasıdır: https://www.hillelwayne.com/formally-specifying-uis/
Ve bazı durumlarda, sonuç iyi tanımlı olmasa bile öğrenilebilir; dolayısıyla mesele sadece oturup neyin anlamlı olacağını düşünmek değildir
Programlama dillerinin tasarımı ve uygulanmasına biraz ilgi duyan biri olarak bu cümle bana gerçekten çok ilginç geldi. “Programlama dilleriyle uğraşan çoğu insan için kolay kısım, programlamayı daha iyi hale getirecek yeni ve daha iyi fikirler üretmektir. Zor kısım ise birini o fikri gerçek işte kullanmaya ikna etmektir”
Buna tamamen katılıyorum. Kazanç olsa bile, yeni bir dile koyabileceğiniz yabancılık miktarının bir sınırı var
Ama AI ajanları, programlama dili tasarımındaki radikal derecede yeni fikirlere büyük direnç göstermeyecektir. Ajanik yapay zekadan sonra programlama dili tasarımının nasıl evrileceğini bir süredir düşünüyorum
Benimsenme kaygısını çok daha az taşırken, programlama dillerini geliştirmek için hangi yeni fikirlerin üretilebileceğini görmek çok ilginç olacak gibi geliyor
https://steveklabnik.com/writing/the-language-strangeness-bu...
Uygulama güvenlik testi tarafında biçimsel yöntemleri uygulama yönünde çalışıyorum ve aynı yaklaşımın iş mantığının doğrulanmasına da uygulanabileceğini düşünüyorum
Bunun için taint analysis kullanıyoruz. Bu, oldukça iyi yerleşmiş bir biçimsel yöntem yaklaşımı, ama gerçek kod tabanlarındaki veri akışı karmaşıklığı nedeniyle sahada hâlâ yaygın biçimde uygulanmış değil
Biçimsel yöntemleri AST desen eşleme ve basit tip denetiminin ötesine taşımak gerçekten zor bir iş. Gerçek kod tabanlarında yordamlar arası veri akışını birkaç dakika içinde izleyip derine gizlenmiş açıkları bulabilen bir taint analysis düzeyine ulaşmak yıllarca Ar-Ge gerektirdi
İlgilenirseniz projeye bakabilirsiniz: https://github.com/seqra/opentaint
Yaklaşık 18 ay önce LLM ile birlikte tipler kullanmaya kapıldım ve
lean4konusunda ciddileşmem 6–8 ay önce oldu. Artık pratik bir C/C++ FFI’si, dolayısıyla fiilen her şeye bağlananCICkanıt temeli olmadan yazılım işlerinde AI desteği kullanmayı düşünmüyorum bileJSON’dan Python’a kadar her şeyi yasakladım;
nix’i bile derleyici içerecek şekilde yeniden yazdım. Kullandığımız neredeyse her şey, sınırına kadar zorlanan property test ve çoklu fuzz testlerden geçmekle kalmıyor, en azından.oleanbağlantısı üzerinden property testleri çalıştıran birlean4kanıtına da sahip. Zaman olduğunda tüm alanın tamlığını bile kanıtlıyor ve o özelliği de test ediyoruzHızlı kısımların hepsi
lean4içinde üretildiği için C++/Rust tartışmasını atlıyoruz. C++ hatasının aslındalean4kodundaki bir hata olduğu durumlarda avantajları var, ama iki tarafa da gidilebilirBu büyük bir değişim ve “JSON ile Python’ı yasaklıyor musun?” diye kuşkulanan insanları suçlamıyorum. Ama biz bu şekilde milyonlarca satırı denetledik ve AI + biçimsel sistemler, AI’sızlıktan AI ve Python’a geçişten çok daha büyük bir sıçrama. İkincisi, bizim deneyimimize göre ilerlemesi tekdüze değil; birincisi ise neredeyse her zaman tekdüze ilerliyor
Oldukça cüretkâr şeyler de mümkün. Bu, ISL ve CuTe benzeri şeylerin modellediği çokyüzlü tensör hesaplarının biçimsel kanıtı; bunu kullanarak C++23’ün
mdspan’i ile cihaz üzerinde swizzling ve tiling yapıp bunun doğru olduğunu da kanıtlayabilirsiniz. Ancak bu örnek, kapsama için L'Hopital tarzı bir argümanı çok iyi göstermiyor: https://github.com/b7r6/mdspan-cuteOrtaya çıkan sonuç gerçekten hızlı, hem de ilk denemeden itibaren hızlı
https://straylight.software/assets/lambda-hierarchy.svg