Neden sadece Lean kullanılmıyor

 (lawrencecpaulson.github.io)
1 puan yazan GN⁺ 1 일 전 | 1 yorum | WhatsApp'ta paylaş
  • Matematiğin formelleştirilme tarihi Lean ile başlamadı; yaklaşık 60 yıl öncesinden beri çeşitli sistem soyları temel teknikleri ve sonuçları zaten biriktiriyordu
  • 1968 tarihli AUTOMATH, LCF ailesi, HOL, Rocq, ACL2 ve Mizar gibi araçlar; reel analizden asal sayı teoremine, dört renk teoreminden Kepler varsayımına kadar geniş bir yelpazede formelleştirme ortaya koydu
  • Lean, büyük kütüphanesi ve canlı topluluğu sayesinde modern matematik tanımlarını hızla biriktirdi; ancak propositions as types ya da bağımlı tipler, proof assistant için tek yol değil
  • Isabelle, güçlü otomasyon, yüksek okunabilirlik ve bağımlı tiplerden kaçınmayı avantaj olarak öne çıkarıyor; ayrıca proof object olmadan da çekirdeğin soyutlama bariyeriyle ispat denetimini kuran LCF geleneğini sürdürüyor
  • Yapay zekanın yapılandırılmış ispatları düzenleyip başka sistemlere çevirme akışı da eklenince, tek bir aracı mutlak ölçüt olarak görmenin yükü gelecekte daha da azalabilir

İlk sistemler ve diğer soylar

  • AUTOMATH

    • AUTOMATH, 1968'de matematik formelleştirmesi için gereken unsurların çoğunu zaten içeriyordu
    • 1977'de Jutting, AUTOMATH ile Landau'nun Foundations of Analysis eserini formelleştirdi ve saf mantıktan başlayıp karmaşık sayıların inşasına kadar ilerledi
    • Eşdeğerlik sınıfları ve rasyonel sayılar kümesini kullandı; reel doğrunun Dedekind tamlığını da biçimsel olarak ispatladı
    • Bu başarı 20 yıl boyunca tekrarlanmadı; reel sayıların yeniden formelleştirilmesi ancak 1990'ların ortasında John Harrison'ın HOL Light'ı ve Jacques Fleuriot'nun Isabelle/HOL'ünde gerçekleşti
    • Gösterim çok elverişsizdi ve hiç otomasyon yoktu; bu yüzden ispatlar uzun ve okunması zordu
    • Buna rağmen eşdeğerlik sınıflarını ele almada Rocq'tan daha iyi olduğu düşünülüyor; Rocq kullanıcılarının yaşadığı setoid hell yerine Jutting, eşdeğerlik sınıflarıyla formelleştirmeyi sakin biçimde yürüttü

  • Boyer ve Moore

LCF sonrası akış

  • Edinburgh LCF, programlama dilleri kuramına odaklanmıştı; ancak proof assistant'ın metadili olarak işlevsel bir dil kullanma fikri geniş ölçüde yayıldı
  • Cambridge, INRIA, Cornell gibi çeşitli gruplar ML kullanarak ilk HOL, Coq (bugünkü Rocq), Nuprl gibi araçları geliştirdi
  • HOL grubu donanım doğrulamaya odaklandı; ancak kayan noktalı donanımın doğrulanması reel analizi gerekli kıldı
  • John Harrison, Cauchy integral formülü üzerinden asal sayı teoremi gibi ciddi matematiksel sonuçları HOL ailesinde ispatladı
  • Mümkün olduğunca çok 100 theorems sonucunu doğrulama hedefi altında HOL Light sık sık en üst sıralarda yer aldı
  • 2014'e gelindiğinde bu soyun sistemleri birçok ileri düzey teoremi formelleştirmişti
  • Bu teoremlerin ispatları genelde uzun ve karmaşıktı; formelleştirme çalışmaları da çok büyük ölçekliydi ve teoremlerde kalan kuşkuları azaltmada kritik rol oynadı

Lean topluluğunun yükselişi

  • Matematikçiler, önceki formelleştirme başarılarının Grothendieck schemes ya da perfectoid spaces gibi ana akım modern matematiğin karmaşık inşalarına kadar uzanmadığını düşünüyordu
  • Tom Hales bu tür tanımları kütüphane olarak biriktirme yönünü seçti, ispattan çok tanımların birikimine odaklandı ve Lean'i tercih etti
  • Bu yaklaşımı Big Proof programında sundu; benzer fikirler de orada tartışıldı
  • Kevin Buzzard bunu duyup eğitimde Lean kullanmayı denemeye karar verince sonrasındaki yayılma hızlandı
  • Lean topluluğunun önemli dönüm noktalarından biri olarak, Rocq'a uzun süre hakim olan yapıcı ispat takıntısından uzaklaşması gösteriliyor
  • Sezgicilik, Russell paradoksundan sonra ortaya çıktı ve reel sayı kavramı üzerinde de belirli sonuçlar doğurdu
  • Martin-Löf type theory açıkça sezgici bir biçimcilik olsa da, Rocq'un bu kadar basit değerlendirilemeyeceği belirtiliyor
  • Buna rağmen Rocq ile ilgili makalelerde yapıcı ispatlar, ilgisiz ya da anlamsız oldukları yerlerde bile tekrar tekrar öne çıktı; bu eğilimin Rocq'un matematikte kullanımını engelleyip alanı Lean'e bıraktığı düşünülüyor

propositions as types ile LCF arasındaki fark

  • Propositions as types, mantık sembolleri ∀, ∃, →, ∧, ∨ ile tip kurucuları Π, Σ, →, ×, + arasındaki ikiliktir
  • Bu çerçeve güzel ve kuramsal olarak üretken olsa da tek yol değildir
  • Proof assistant'ı, propositions as types ilkesine göre ispat denetleyen yazılımla sınırlamak, son yarım yüzyılın araştırmalarının büyük bölümünü tanımın dışına iter
  • O durumda geriye yalnızca Rocq, Lean ve Agda kalır
  • Hatta AUTOMATH bile propositions as types örneği değildir; Π ve → benzeri unsurları olsa da mantığı, sıradan mantık ders kitaplarında olduğu gibi aksiyomlar olarak kurar
  • de Bruijn, 50 yıl önce bile tipler ile önermelerin ayrılması gerektiğini düşünüyordu
  • Örneğin bölme işlemi üç argüman almalıdır; çünkü (x/y) değerinin (y \ne 0) ispatına bağlı olması proof irrelevance gerektirir
  • LCF yaklaşımının propositions as types ile aynı olduğu yönündeki algının da gerçeği yansıtmadığı özellikle vurgulanıyor
  • Rocq ve Lean'de, önermelerin sort'u olan Prop bulunur; burada aynı önermenin bütün proof object'leri aynı değer olarak değerlendirilir ve bu sayede proof irrelevance sağlanır
  • Ancak bu, devasa ispat nesnelerinin ortadan kalktığı anlamına gelmez; bunlar gerçek sistemlerde hâlâ vardır
  • Robin Milner'ın temel keşfi, LCF'de ispat nesnelerinin kendisine gerek olmamasıydı
  • İspat çekirdeği ML'nin soyut veri tipi içine yerleştirilip çıkarım kuralları kurucu yapılırsa, ispatlar dinamik olarak denetlenebilir
  • ML'nin abstraction barrier'ı sayesinde hile yapmanın imkânsız olduğu düşünülür
  • Hiçbir şeyi işaret etmeyen devasa terimlerin onlarca MB yer kaplaması, RAMmageddon çağında özellikle mantıksız görünüyor
  • Bu gereksiz terimleri daha zarif hale getirmeye yönelik araştırmaların sürmesi de eleştiriliyor

Isabelle'i seçmek için nedenler

  • Çevrenizdekiler Lean kullanıyorsa, ekibin uzmanlığı Lean üzerindeyse ve gereken öncül kütüphaneler de Lean'deyse Lean kullanmak doğaldır
  • Yine de özgürce seçim yapılabiliyorsa Isabelle'i değerlendirmek için açık nedenler vardır

  • Otomasyon

    • Avantaj olarak en güçlü otomasyon gösteriliyor; günlük “hammer” araçlarıyla karşılaştırıldığında sledgehammer ile boy ölçüşebilecek bir şey olmadığı söyleniyor
    • Bilgisayarlı cebir tarafının da ayrıca ele alınması gerektiği belirtiliyor

  • Okunabilirlik

    • Okunabilirlik açısından en iyi seçenek olarak görülüyor ve buna dayanak olarak Isar örnekleri veriliyor

  • Bağımlı tiplerden kaçınma

    • Bağımlı tipler olmadığı için universe level ve yeni başlayanları zorlayan çeşitli tuhaflıklardan kaçınılabiliyor
    • Lean'in mathlib'i ile Rocq'un SSReflect ve Mathematical Components ekosistemlerinde de bağımlı tip kullanımının teşvik edilmediği belirtiliyor
    • Bağımlı tiplerin temel zorluğu, doğru şekilde uygulanırlarsa tip denetiminin kendisinin karar verilemez hale gelmesidir
    • Bunun nedeni eşitlik kararının karar verilemez olmasıdır; ilk dönemlerde bunun doğal karşılandığı ifade ediliyor
    • Yaklaşık 1990'dan itibaren, tip denetimini karar verilebilir kılmak için eşitliği definitional/intensional equality düzeyine indirme yönünde bir uzlaşma oluştu
    • Sonuç olarak (T(N+1)) ile (T(1+N)) farklı tipler haline geldi
    • Bu sınırlamalar gerçek ispatları da etkiliyor ve definitional equality denetiminin kendisi de hâlâ hesaplama açısından maliyetli

Bağımlı tipler olmadan da modern matematik mümkün

  • 2017 itibarıyla Isabelle'in hangi düzeyde matematiği kaldırabileceği konusunda çok daha temkinli olunduğu belirtiliyor
  • O dönemde aşağıdaki konuları ele almak için bağımlı tiplerin zorunlu olduğu kolayca düşünülebilirdi
  • Ancak Alexandria ile ilgili araştırmalar sayesinde çok şey öğrenildi ve temel noktanın her şeyi tiplerin içine sıkıştırmamak olduğu sonucuna varıldı

Geleceğin yönü ve yapay zeka

  • Lean birçok şeyi doğru yapıyor ve iç içe geçmiş ispat bloklarını da desteklediği için, potansiyel olarak yeterince okunabilir bir ispat dili olabilir
  • Artık Lean topluluğunun bu özellikleri gerçekten kullanması gerekiyor; Isabelle kullanıcılarının ise büyük ölçüde bunu zaten yaptığı belirtiliyor
  • Bilgisayarın denetleyebildiği ispat nesnelerinden çok, insanların gerçekten okuyabildiği ispat metninin saydamlığı daha önemli
  • Yapay zekanın yükselişi bu farkı daha da görünür kılıyor
  • Yapay zekanın ürettiği ispatlar çoğu zaman dağınık oluyor; ama sledgehammer ile toparlanmaları kolay ve yapı iyi kurulmuşsa ayrıntı fazlalığına rağmen okunabiliyorlar
  • Bu sayede ilerleyişin akışını kavramak ve daha sade bir biçime indirgemek kolaylaşıyor
  • Son dönemde, dil modellerinin doğrudan sledgehammer çağırdığı araştırmalar da ortaya çıktı
  • Yapay zeka, okunması kolay yapılandırılmış ispatları bir proof assistant'tan diğerine çevirme işini de kolayca yapabilir
  • Böyle olursa hangi sistemin seçileceğine ilişkin yük de azalır

Mizar eksikliğinin tamamlanması

  • Matematiğin formelleştirilme tarihi, Mizar ve onun devasa matematik kütüphanesi olmadan tamamlanmış sayılamaz
  • Isabelle'in Isar dili de Mizar'dan büyük ölçüde etkilendi
  • Mizar'ın atlanmış olması özellikle düzeltiliyor ve sonraki yazıda Mizar'ın ele alınacağı belirtiliyor

İlgili okumalar

1 yorum

 
GN⁺ 1 일 전
Hacker News görüşleri

  • HN okurlarının çoğu matematikçiden çok programcıya daha yakın olduğu için, Lean’e matematiksel kanıttan ziyade programlama açısından bakmanın daha pratik olduğunu düşünüyorum
    Lean’i fonksiyonel programlama perspektifiyle ele alan kitaplardan https://leanprover.github.io/functional_programming_in_lean/ oldukça iyi
    Ben de Lean öğreniyorum, o yüzden acemiye özgü biraz pembe bir bakışım olabilir; ama son dönemde lean-zip örneğinde olduğu gibi gerçek sıkıştırma/açma algoritmaları gibi sıradan programcı kodlarını yazıp kanıtlayabilmeyi hedefliyorum
    https://github.com/kiranandcode/lean-zip/blob/master/Zip/Nat...

    • Bu kitabı okurken Lean ile temel bir bilgisayar cebiri sadeleştiricisi üzerinde biraz oynadım
      https://github.com/dharmatech/symbolism.lean
      C# kodunun bir portu ve Lean’in ifade gücü şaşırtıcı derecede yüksek
    • Böyle bir kullanım için Dafny de benzer bir seçenek sayılmaz mı diye düşünüyorum
      Bir ara biraz gündem olmuştu, ama son dönemde bu alanı yakından takip etmedim
    • 1990’larda yazılım doğruluk kanıtı denemeleri yapılan bir örneği hatırlıyorum; nihai kanıt açıklamaları kısmında gerçek yazılımdan daha fazla hata çıkmıştı diye hatırlıyorum
      Ayrıca iki engel daha görüyorum. Birincisi, yazılımın ne yapması gerektiğini bilmek başlı başına zor ve kullanıcının yapmak istediği şeyle müşterinin para ödediği şey de her zaman aynı olmuyor
      İkincisi, birçok geliştiricinin iş kalitesi o kadar düşük ki Java gibi dillerden daha iyi hakikat dili kullanmalarını beklemek zor
      Ama ikincisi, gereken özeni gösteren AI sistemleriyle yer değiştirdikçe ortadan kalkabilir; o zaman tablo değişebilir
    • Fonksiyonel olmayan programlama için durum ne diye düşünüyorum
      Fonksiyonel programlamanın da, çoğu programcı için çok da ilgili olmayan ve çoktan geride bırakılmış matematik kadar alakasız kaldığını düşünüyorum

  • Yazarın Lean’i epey yanlış anladığı anlaşılıyor; alanı iyi bilen biri gibi göründüğü için bu daha da şaşırtıcı
    Lean’in kanıt nesnelerini olduğu gibi koruduğunu ve sonunda tüm tanımların açıldığı devasa bir kanıt nesnesini denetlediğini sanıyor gibi, ama bu gerçekle pek örtüşmüyor
    Lean, yazarın LCF’nin avantajı diye övdüğü optimizasyonu fiilen neredeyse birebir uyguluyor. Bir benzetmeyle, kanıtı tahtayı silerek ilerletmek gibi
    Lean4’te def yerine theorem ile yazarsanız, o kanıt nesnesi artık kullanılmaz; bu sadece bir optimizasyon değil, dilin temel özelliğidir. theorem opaque’tir
    Kanıt terimi ortada kalsa bile bunun tek nedeni etkileşimli modda kullanıcıya gösterilebilmesidir; kernel ise o kanıt nesnesinin ne olduğuyla ilgilenmez bile

    • Bu, uygulamadan çok kavramsal bir fark gibi
      LCF’de kanıt ve terim farklı şeylerdir ve bence aslında öyle olması gerekir. Bu tür Curry-Howard tarzı karışıklık gereksiz; ama birçok kişi bilgisayarla matematik yapmanın tek yolunun bu olduğunu sanıyor
      İsterseniz LCF’de de kanıtları saklayıp kullanabilirsiniz, Lean’de de isterseniz optimizasyonla ortadan kaldırabilirsiniz
    • Bağımlı tip teorisinde kanıt nesnesi, yalnızca belli bir tipi dolduran terimin kendisi olduğuna göre, Lean uygulamasının böyle terimler üretmeden kanıt inşa edebilmesi mi kastediliyor diye merak ediyorum
    • Doğru gibi görünüyor
      Soyut tip yaklaşımı biraz bellek kazandırabilir ama bu yalnızca sabit katsayı düzeyinde bir farktır, asimptotik bir iyileşme değildir
      Lean’in onlarca MB harcadığından şikâyet etmek 1980’ler ve 90’larda önemli olabilirdi ama bugün o kadar belirleyici bir avantaj olmayabilir

  • Lean’in fonksiyonel programlama için iyi olduğunu sık duyuyorum ama Agda’dan gelince biraz kaba bir geriye gidiş gibi hissettiriyor
    tactic’lerin de iyi olduğu söyleniyor ama benim deneyimimde Coq tactic’leri daha güçlü ve kullanımı daha kolaydı
    Bu tamamen ilk izlenim yanlılığı da olabilir, ama şimdiye kadar Lean’in gücü bir şeyi herkesten iyi yapmasından çok, genel olarak yeterince iyi olması ve topluluğunun büyük olmasında gibi görünüyor
    Neden çekici olduğunu anlıyorum ama bunun bedeli olarak biraz güzellik ve güç kaybolmuş gibi, o da üzücü

    • Sonuçta bu bir tür ağ etkisi meselesi
      Ama bu tür etkiler o anda kalıcıymış gibi görünse de gerçekte sanıldığından kısa sürebilir. Sadece bu önemli olsaydı, Perl bugün hâlâ devlerden biri olurdu
      Lean özelinde özellikle önce büyük bir kütüphane edinmiş olması önemli. Perl için CPAN neyse o gibi
      Ama ölçekleme yasalarına bakınca, çoğu kullanıcı için büyük bir kütüphanenin değeri muhtemelen boyutunun logaritması kadar artar
      https://pdodds.w3.uvm.edu/teaching/courses/2009-08UVM-300/do...
      Başta bu fark kapatılamaz gibi görünür ama bir noktadan sonra sırf ölçeği yakalamak değil, kullanılabilirlik daha önemli hale gelir
      Üstelik matematik kütüphanesi port etmek LLM’lere çok uygun bir iş. Kaynak doğrulanmış, hedef doğrulanabilir ve akıl yürütme yolu da büyük ölçüde taşınabilir
      Tersinden bakarsanız, LLM’ler sayesinde küçük platformlarda çalışmanın eşiği de beklenenden daha düşüyor. O taraftaki kütüphaneyi kendi platformuma taşıyabiliyorsam, kendi kanıtımı da oraya taşıyabilme ihtimalim yüksektir
    • Hatta bu daha çok topluluğun sonunda olgunlaşıp gerçek işler yapmaya başladığını gösteriyor gibi
      Mükemmel araç asıl mesele değil; yeterince iyi bir araçla işi bitirmek daha önemli
    • Agda kanıt denetleyicisi olarak daha iyi olabilir ama yazılım geliştirmek için pratik bir seçenek olduğunu düşünmüyorum
      Lean, gerçekten Haskell’in halefi olabilecek kadar yazılım geliştirmeye uygun bir fonksiyonel dil haline gelme potansiyeli taşıyor gibi görünüyor
    • Agda’yı biraz, Lean’i ondan daha fazla kullandım; matematiksel kanıtlardan çok genel fonksiyonel programlar yazmak Lean’de çok daha kolaydı
      Fark büyük ölçüde araç desteğinden geliyordu sanırım. Agda belgeleri zayıf, sistemi kurup çalıştırmak zahmetli ve fiilen Emacs kullanmanızı güçlü biçimde dayatıyor
      Buna karşılık Lean’in kendi belgelerinde cat yardımcı programının nasıl yazılacağı bile var ve genel olarak çok daha modern bir tooling deneyimi sunuyor
    • Agda’nın fonksiyonel programlama tarafında tam olarak neyin daha iyi olduğunu merak ediyorum
      Genelde övgüyü daha çok dependent pattern matching konusunda duyuyorum; o noktada Lean bana oldukça zayıf geliyor
      Yine de genel FP’de de Agda’yı daha dostça buluyorsanız, hangi açılardan olduğunu duymak isterim

  • Isabelle/HOL’un dili kendi başına fena değil ama tooling tarafında, masaüstü merkezli yaklaşımını bir yana bıraksak bile, derin kusurlar var
    Dil Lean’den mutlaka daha iyi değil, sadece farklı ve bağımlı tiplere yönelik bazı eleştirilere katılıyorum
    Sonuçta iki dil de farklı ödünleşimler yapmış ve bu seçimler onları kendi alanlarında epey verimli araçlara dönüştürmüş gibi. Kanıt alanı başlı başına geniş; her paradigmanın güçlü ve zayıf yanları var ve Lean bunların başka bir kısmında uzmanlaşmış durumda
    Sledgehammer iyi ama Lean’de de benzeri bir şeyin ortaya çıkması zaman meselesi gibi
    Keşif aşamasında yararlı olabilir ama çok kaynak tüketiyor; kanıtları kısaltıyor olsa da açık kodda yarı büyülü by sledgehammer yerine kanıtın tüm adımlarının doğrudan görünmesini tercih ederim
    Buna karşılık Isabelle’in kendisini geliştirmek, Lean’e kıyasla çok daha acı verici; özellikle de geliştiricilerle iletişim kurma kısmı
    E-posta listesinde hata yoktur, sadece beklenmedik davranış vardır tarzı tutum çocukça ve profesyonellikten uzak görünüyordu
    Ayrıca Lean benzeri sistemlerin RAM kullanımını küçümsemek de, Isabelle tarafındaki bellek oburluğu düşünülünce oldukça komik

    • Buradaki sorun, UNSAT sertifikasını hızla denetlenebilir bir biçime dönüştürmenin hiç de önemsiz olmaması
      Aslında bu neredeyse başlı başına biçimsel kanıt yazmak kadar zor
    • En son baktığımda Isabelle/HOL arayüz olarak özel bir Emacs modu kullanıyordu diye hatırlıyorum
      Başka bir HOL ile karıştırıyor da olabilirim
    • Sledgehammer’ın ne olduğunu bilmiyorum ama anlatılandan, Mathlib’deki grind ile neredeyse aynı türden bir araç gibi geliyor
      https://leanprover-community.github.io/mathlib4_docs/Init/Gr...

  • Lean’de ilginç olan şey, Lean’in bir dil olması ama insanların asıl konuştuğu şeyin çoğu zaman aslında Mathlib adlı kütüphane olması
    Mathlib’i yapanlar oldukça pragmatik görünüyor; bu yüzden de Lean tiplerinin içine klasik mantığı yerleştirip sezgici mantığı sadece kısmen kullanıyorlar gibi

    • Üçüncü halin imkânsızlığı anlatılırken verilen örnek yanlıştı
      “Bir şey aynı anda hem doğru hem yanlış olamaz” ifadesi üçüncü halin imkânsızlığı değil, çelişmezlik ilkesidir
      Üçüncü halin imkânsızlığı, p doğru ya da not p doğrudur demektir
      https://en.wikipedia.org/wiki/Law_of_noncontradiction
    • Bilgisayar bilimi tarafı artık kendi CSLib’ini oluşturuyor
      https://www.cslib.io https://www.github.com/leanprover/cslib
      Sezgici mantık özünde matematiksel akıl yürütmeyi hesaplanabilir yapılara dönüştürmekle ilgili olduğundan, bu meseleye nasıl yaklaşacakları ilginç
      Aslında Lean ile algoritma yazdığınız anda zaten bir şekilde yapıcı kısıtların içine giriyorsunuz ve o amaç için bu kadar mantık yeterli olabilir
    • Yapıcı matematiği kabullenmenin 5 aşaması esprisi aklıma geldi
      inkâr, öfke, pazarlık, depresyon, kabullenme
      Andrej Bauer’in ilgili konuşması ve yazısı da bakmaya değer
      https://www.youtube.com/watch?v=21qPOReu4FI
      http://dx.doi.org/10.1090/bull/1556
    • Burada kastedilen intuitive logic değil, intuitionistic logic olmalıydı
    • Bunca kısıt ve tıkanmaya rağmen, insanların ne zaman ve neden sezgici mantığı tercih etmeye başladığını merak ediyorum

  • Bence bu tür yazılara daha fazla ihtiyaç var
    Herkesin kendiliğinden doğruymuş gibi sadece X kullan diye dayattığı grup düşüncesine karşı, en azından alternatifleri değerlendirmek için her zaman ikna edici sebepler bulunabilir
    Sonunda alternatifi bırakıp ana akımı seçseniz bile, araziyi bilerek karar vermek daha iyidir

    • Buna tamamen katılmıyorum
      Şu anda bile çok fazla framework ve alternatif üretiyoruz; muhtemelen eğlenceli olduğu için daha da fazla üretiliyor
      Mevcut araçları iyileştirmek ya da sadece gerçek işi ilerletmek yerine, sürekli yeni dil, kütüphane ve derleme aracı eklemeye gidiliyor
      Bugünkü dil, kütüphane ve build tool sayısı yarısı kadar olsaydı bence daha iyi olurdu
    • Sonuçta duruma bağlı
      Ana akımdan ne kadar uzaklaşırsanız belge o kadar azalır, daha az keşfedilmiş köşeler yüzünden hata sayısı artar ve yardım alabileceğiniz insan sayısı düşer
      Seçenek sayısı yirmiyi geçtiğinde, ortalamada standart seçeneği alıp devam etmek doğrudur. Dikkat sınırlı; her bağımlılık için araştırma raporu yazarsanız asıl problemi çözemezsiniz
      İki istisna var: standart araç gerçekten benim kullanım durumuma uymuyorsa ya da standart aracın kendisi çözmeye çalıştığım temel sorunla büyük ölçüde çakışıyorsa

  • Bu tartışmalar bana Python’un bilimsel hesaplamadaki sınırlarını anlatan yazıları hatırlatıyor
    Yeterince iyi bir aracın etrafında topluluk kritik kütleyi aşacak kadar birikince, bu diğer unsurların çoğunu gölgede bırakıyor
    İvme oluşuyor; eğitimler, açıklayıcı yazılar ve daha iyi belgeler birikiyor ve sonunda fiilen kaçış hızına ulaşılıyor
    Lean, Terrance Tao gibi güçlü destekçileri de olduğu için tam şu anda böyle bir yerde gibi görünüyor
    O yüzden “X dili daha iyi” demek tamamen yanlış olmasa da asıl önemli soruyu kaçırmak kolay
    Esas mesele, herkesin bildiği, hemen kullanabildiği ve geliştirilmesine daha fazla zaman ayrılan araçtan gerçekte daha iyi olup olmadığı
    Sonuçta bu biraz worse is better ya da iyi ve popülerse bunun yeterli olduğu bir durum gibi görünüyor

    • LLM’lerin farklı biçimsel sistemler arasında çeviri işini oldukça etkili kılabilecek olması bence iyi bir nokta
      Özellikle bu alanda çeviri çıktısını büyük ölçüde otomatik doğrulamak mümkün olduğu için, seçim o kadar da büyük mesele olmayabilir
    • Ama AI çağında kritik kütlenin önemi çok daha az
      AI, devasa topluluk kütüphaneleri olmasa da kendi başına kod yazabilir ve internette milyonlarca eğitim metni dolaşmasa da belgeyi ve spesifikasyonu doğrudan okuyabilir
      İş piyasası olmayan dillerden kaçınmak da gerekmez. AI kariyer inşa etmiyor; sadece o anda verilen işi yapıyor
      Bu yüzden eskiden şansı olmayacak küçük diller ve DSL’ler için bile benimsenme ihtimali artıyor
      Programlamada uzun süredir devam eden dil tek kültürünü de AI’nin sona erdirebileceğini düşünüyorum

  • “Bugün herhangi bir sistemle biçimselleştirilen neredeyse her şey AUTOMATH ile de biçimselleştirilebilirdi” sözü, bugün modern dillerle yazılan her şeyin 50 yıl önce assembly ile de yazılabileceğini söylemeye benziyor
    Teknik olarak doğru olabilir ama ekonomik olarak tamamen farklıdır

    • Assembly dilleri genelde Turing-tamdır; kanıt motorları tarafında buna tam olarak karşılık gelen kıyasın ne olduğunu ben de pek bilmiyorum

  • Yaklaşık 15 yıl önce Coq/Rocq ve birkaç başka aracı kurcalamaya çalıştım ama kavramlardan çok yazılımın kendisini anlamak imkânsız gibi gelmişti
    Kanıt asistanları / etkileşimli teorem ispatlayıcılardaki tuhaflık şu: interactive olmaları yüzünden dil ve IDE birleşik bir hale geliyor ve pratikte de ikisi güçlü biçimde birbirine bağlanıyor
    Bu yüzden dili tek başına konuşmak zor; hangi ortamda kullanıldığına da bakmak gerekiyor
    Ben de VS Code’un fanatik bir hayranı değilim ama çok sayıda insanın kullandığı, büyük paralar harcanarak olgunlaştırılmış genişletilebilir IDE’nin alternatiflerin sunduğu ortamlardan çok ileride olduğu açık
    Natural Numbers Game gibi harika bir başlangıç yolu da sanki VS Code’un hacklenebilirliği ve ekosistemi sayesinde mümkün olmuş gibi
    Ama Lean öğrenirken beni kaygılandıran şey, söz dizimi genişletilebilirliğinin iki ucu keskin bir bıçak olması
    Dili öğrendikten sonra o dilde yazılmış kodu okumak istersiniz; ama projeler kendi DSL’lerini yığmaya başlarsa bu kontrolden çıkabilir
    Sonuçta bu, topluluğun ve ekosistemin ne kadar ölçülü davranacağına bağlı; o yüzden biraz umutla biraz da kaygıyla izliyorum

  • Lean, matematikçiler tarafından en çok sevilen kanıt asistanı da değil, yazılımın biçimsel doğrulanması için en uygun araç da değil
    Ama ikisini de idare eder düzeyde yapıyor ve karşılığında elde edilmesi en zor şey olan ivmeyi yakalamış durumda
    Üstelik AI çağında herkese açık insan eliyle yazılmış kod miktarı, ajanların yeni kodu ne kadar iyi üretebildiğini doğrudan etkilediği için, bu ivme daha da güçleniyor