Kafanızda küçük ispatlar kurarak daha iyi bir programcı olmanın yolu

 (the-nerve-blog.ghost.io)
1 puan yazan GN⁺ 2025-07-16 | 1 yorum | WhatsApp'ta paylaş
  • Daha iyi bir programcı olmak için kod yazarken kafanızda küçük ispatlar kurma alışkanlığı edinmek önemlidir
  • Monotonicity, immutability, pre- ve post-condition'lar, invariant'lar gibi kavramlar bu mini ispatları yaparken temel rol oynar
  • Kod değişikliğinin tüm sistem üzerindeki etki alanını (izolasyon, firewall) dikkate alarak tasarlamak, karmaşıklığı ve riski azaltmada büyük fayda sağlar
  • Tümevarım kullanıldığında özyinelemeli fonksiyonların veya yapıların doğruluğu adım adım ispatlanabilir
  • Bu düşünme biçimi pratik ve alışkanlıkla gelişir; gerçek matematiksel ispat çalışmaları ve algoritma problemi çözümü bu konuda büyük yardım sağlar

Giriş ve temel fikir

  • Yazar, kariyeri ilerledikçe kodun doğruluğunu ve geliştirme hızını artırmak için doğal olarak "küçük ispatlar kurma alışkanlığı" edinmiş
  • Kod yazarken beklenen davranışı zihinde doğrulama ve akıl yürütme süreci pratik gerektirir; ustalaşıldığında kodun kalitesi gözle görülür biçimde artar
  • Bunu tam olarak nasıl yaptığınızdan çok, farklı yöntemlerle kendinize uygun biçimde pratik etmeniz önemlidir

Monotonicity

  • Monotonicity, bir fonksiyonun ya da kodun yalnızca tek yönde ilerleme özelliğini ifade eder
  • Örnek olarak checkpointing verilebilir; burada iş adımları yalnızca ileri gider ve tamamlanmış işler geriye dönülerek yeniden çalıştırılmaz
  • LSM tree ile karşılaştırılan B-tree örneğinde, LSM tree çoğu durumda alanı biriktirir ve yalnızca compaction sürecinde küçülür
  • Monotonicity garanti edildiğinde karmaşık durumların veya sonuçların bir kısmı doğal biçimde elenebilir ya da öngörülebilir
  • Immutability de benzer bir kavramdır; bir kez ayarlanan değer artık hiç değişmediği için olası durum değişimleri dışlanabilir

Pre- ve post-condition'lar

  • Pre-condition ve post-condition, bir fonksiyon çalışmadan önce ve sonra mutlaka doğru olması gereken iddialardır
  • Fonksiyon yazarken bu koşulları açık biçimde takip etmek, mantıksal düşünme ve test açısından faydalıdır
  • Post-condition'ları net tanımlamak, unit test case'lerini daha kolay çıkarmayı sağlar
  • Koda bu koşulları doğrulayan assertion'lar ekleyerek beklenmeyen durumlarda erken durması sağlanabilir; bu da öngörülebilirliği ve güvenliği artırır
  • Bazen bir fonksiyona net pre-/post-condition'lar vermek başlı başına zor olabilir; bunu fark etmek bile önemli bir içgörü sağlar

Invariant'lar

  • Invariant, kodun her durumda; çalışmadan önce, çalışırken ve çalıştıktan sonra daima doğru kalması gereken özelliğidir
  • Örneğin çift taraflı muhasebedeki muhasebe eşitliği tipik bir invariant örneğidir (toplam alacak = toplam borç)
  • Kodu küçük adımlara bölüp her adımın invariant'ı koruduğunu ispatlamak, bütünün tutarlılığını güvence altına alır
  • Invariant'ları korumak için listener'lar veya lifecycle method'lar kullanılabilir (C++ constructor/destructor, React useEffect gibi)
  • Değişiklik noktaları az olduğunda veya akış yolları basit olduğunda invariant doğrulaması çok daha kolay olur

İzolasyon

  • İyi yazılımın temel özelliklerinden biri, mevcut sistemi kararsızlaştırmadan yeni özellik ekleyip değiştirebilmektir
  • Kod değişikliğinin etki yarıçapını (blast radius) anlamak ve yapısal firewall'lar oluşturarak etkinin yayılacağı alanı en aza indirmek gerekir
  • Gerçek hizmet Nerve örneğinde, query planner ile query executor arasındaki sınırın net tanımlanması ve değişikliklerin bu sınırı aşmamasını sağlayan tasarımdan söz edilir
  • Gereksiz değişiklik yayılımı engellendiğinde doğrulama ve bakım kolaylaşır, kararlılık artar
  • Bu yaklaşım, OCP (Open-Closed Principle) felsefesiyle de örtüşür: mevcut davranışı değiştirmeden işlevi genişletmek

Tümevarım

  • Birçok program özyinelemeli fonksiyonlar veya özyinelemeli yapılar içerir ve bunların mantığını kurarken tümevarım güçlü bir araçtır
  • Özyinelemeli bir fonksiyonun davranışını ve doğruluğunu adım adım ispatlamak için base case ve inductive step ayrı ayrı doğrulanmalıdır
  • Örnek olarak AST (syntax tree) yapısındaki düğüm sadeleştirme süreci verilir; her aşamadaki tümevarımsal argümanlarla invariant'ların korunduğu ve davranışın doğru olduğu gösterilir
  • Tümevarımsal düşünme içselleştirildiğinde özyinelemeli kod yazmak ve doğrulamak çok daha sezgisel ve kolay hale gelir
  • Tümevarımsal olmayan, bütüncül (holistic) doğrulama denemeleriyle karşılaştırıp hangi yaklaşımın daha doğal geldiği üzerine düşünmeye değerdir

Bir kalite ölçütü olarak Proof-affinity

  • Yazar, kafada küçük ispatlar kurmaya elveren kodun iyi kod olduğunu savunuyor
  • Kod monotonicity, immutability, açık koşullar, invariant ayrımı, firewall sınırları ve tümevarım kullanımı gibi yapılara sahipse ispatlanması kolaylaşır; dolayısıyla kod kalitesi de yükselir
  • Kodun anlaşılması zor ve doğrulanması güçse bu durum, refactoring ya da yapıyı yeniden düşünme ihtiyacına işaret eder
  • Bu bağlamda yazar, "kanıtlanabilirlik" yerine proof-affinity terimini öneriyor
  • Proof-affinity yazılım kalitesinin tek unsuru olmasa da, kodu anlama, genişletme, test etme ve sürdürmede çok önemli bir hızlandırıcıdır

Yetkinliği artırma yolları

  • Bu mantıksal düşünme biçimi, ancak yeterli pratikle bilinçdışı düzeyde doğal biçimde uygulanır hale gelir
  • Sık sık (matematiksel) ispat yazmak ve mantıksal akıl yürütme becerisini geliştirmek şarttır
  • Algoritma problemi çözmek de (Stanford'un EdX dersleri, Leetcode vb.) iyi bir antrenman alanıdır; yalnızca püf noktası içeren sorular yerine dikkatli implementasyon ve ispat benzeri düşünme gerektiren problemlere odaklanmak daha verimlidir
  • Sonucu defalarca düzelterek doğruya ulaşmaya çalışmak yerine, ilk denemede doğru cevaba mümkün olduğunca yakın gitmeyi hedefleyen pratik önemlidir
  • Bu alışkanlıklar yerleştikçe mantıksal sistem tasarımı ve kod kalitesi büyük ölçüde gelişir

İlgili okumalar

1 yorum

 
GN⁺ 2025-07-16
Hacker News görüşü

  • Bu konuya tam uyan, basit ama şaşırtıcı bir örnek var: ikili arama. Sol/sağ varyantları da var ama döngü değişmezlerini düşünmezsen doğru şekilde uygulamak çok zor. Bu yazı değişmez temelli yaklaşımı ve buna uygun Python kodu örneğini açıklıyor. Programming Pearls yazarı Jon Bentley, IBM programcılarından sıradan bir ikili arama yazmalarını istediğinde %90'ında hata vardı. Çoğu sonsuz döngüye giriyordu. O dönemde tamsayı taşmasını da elle önlemek gerektiği için bir yere kadar anlaşılır ama oran yine de şaşırtıcı

    • Bunu gördükten sonra mülakat sorusu olarak ikili arama kullanmaya başladım. Tanınmış adayların yaklaşık 2/3'ü 20 dakika içinde doğru çalışan bir uygulama yazamadı. Özellikle kolay durumlarda sonsuz döngüye girenler çoktu. Başaranlar ise hızlıca yaptı. Sorunun nedenlerinden biri, çoğu kişinin hatalı bir arayüzle öğrenmiş olması olabilir. Wikipedia açıklaması da "L'yi 0, R'yi n-1 olarak başlat" diyor; bu, R'nin dahil olduğu bir aralık. Oysa pratikte çoğu string algoritmasında üst sınırın dahil edilmediği, yani R'nin n olduğu biçim daha iyi. Bu hipotezi doğrudan test etmek isterdim. Farklı fonksiyon prototipleri ve başlangıç değerleriyle çok sayıda kişiye yazdırıp inclusive ve exclusive upper bound ile length yaklaşımında ne kadar hata çıktığını karşılaştırmak isterim

    • Aslında ikili arama, indeks yönetiminin neredeyse en uğraştırıcı olduğu klasik örnek. Hoare partition algoritmasıyla birlikte hatasız ve doğru kodlaması en zor temel algoritmalardan biri

    • Test olsun diye Claude Sonnet'e hatasız ikili arama Python kodu yazdırdım

    def binary_search(arr, target):
    left = 0
    right = len(arr) - 1
    while left <= right:
        mid = left + (right - left) // 2
        if arr[mid] == target:
            return mid
        elif arr[mid] < target:
            left = mid + 1
        else:
            right = mid - 1
    return -1

    Örnek diziyle çeşitli test durumlarını da doğruladım

    • İkili aramadaki hataların kötü örnek uygulamalar yüzünden meşhur olduğunu öğrenince, kitaba hatasız ilk uygulamayı koymayı denedim. Gerçekten çok dikkatli yazdım ama yine de bir hata çıktı; epey komik. Neyse ki Manning'in ön geri bildirim sistemi sayesinde baskıdan önce düzeltebildim

    • Ben sol/sağ ikili arama uygulamalarını her zaman "şimdiye kadarki en iyi değeri" hatırlayarak yazıyorum. C++'taki lower_bound, upper_bound gibi. while (l < r) yapısında orta noktayı bulup mevcut konumu kontrol ederek aralığı uygun şekilde daraltıyorum. Mesela upper_bound için sol sınırı yükseltiyor, lower_bound için sağ sınırı indiriyorum. Uzun zaman sonra tekrar leetcode çözüyorum, kafam biraz durmuş olabilir; format dağınık olabilir

  • Uzun zaman önce yüksek lisans dersinde buna benzer bir kavram öğrenmiş olabilirim. Lisansın sonlarına doğru matematik sınavlarını tamamen tükenmez kalemle çözmeye başlamıştım. Nedenini pek bilmiyordum ama notlarım hep yüksekti; çünkü çözümleri tek seferde ilerleyerek yazmadan önce tüm ispat akışını zihnimde netleştiriyordum. Bu sayede hatalarım çok azaldı. Kod yazarken de benzer şekilde, işe başlamadan önce tasarımı zihnimde iyice olgunlaştırıyorum

  • Daha iyi bir programcı olmak istiyorsan, kod için küçük ispatlar yazma alışkanlığı edinmelisin Testler ve tip tanımları tam olarak buna örnek Özellikle önce test, sonra tipler, en son kod sırasıyla ilerliyorum Her acceptance criteria için test yazıyor, girdi/çıktının açıkça anlatıldığı testler hazırlıyorum Bir API ise önce OpenAPI ya da GraphQL ile tüm alanları ve tipleri içeren bir sözleşme tanımlayabilirsin. Çalışma anında bu sözleşmeye dayanarak veri doğrulaması yapılabilir ve bu sözleşmenin kendisi de uygulamanın spec'e uygun çalıştığının kanıtı olur Özetle OpenAPI/GraphQL, testler ve tipler sayesinde sistemin gerçekten amaçlandığı gibi çalıştığına dair kanıt elde etmek önemli Spec'i baştan iyi tasarlarsan, kod uygulamasını esnek biçimde değiştirebilir ama doğruluğu spec üzerinden kanıtlamaya devam edebilirsin Kodun kendisinden çok spec daha önemli

    • Yazıda bahsedilen beş özellik iyi bir tip sisteminde ifade edilebilir. Böylece spec'in önemli bir kısmı doğrudan kod olur ve derleyici doğruluğu garanti eder. Programlamanın geleceği, bu yaklaşımın doğal kabul edildiği bir yer olmalı OpenAPI ve GraphQL'in tip sistemleri çok zayıf; böyle bir geleceğe ulaşmak için daha 50 yıl gelişmeleri gerekir

  • Üniversitede kuramsal bilgisayar biliminin temellerini öğrendim ve yazının ana fikrine katılıyorum. Uygulaması kolay değil Önkoşul/sonkoşullara ek olarak, loop invariant ve structural induction gibi CS ispat teknikleri çok güçlü loop invariant, structural induction bağlantılarıyla birlikte UofT CSC236H ders notlarını da öneririm (ders notları)

    • Bu CSC236 ders notları gerçekten çok iyi ve Prof. David Liu da harika biridir öğretim üyesi profili

    • UofT'den bahsedilmiş! Hoşuma gitti

  • "Kod hakkında zihninde küçük ispatlar kurmaya çalış" fikri, neredeyse kendiliğinden açık olacak kadar önemli bir ilke. Kodun her parçasının ne yaptığını anlatan kısa bir önermeyi sürekli akılda tutmalısın

    • Bu yaklaşım greenfield projelerde, yani yakın zamanda tüm kodu kendin yazdıysan kolay; ama farklı fonksiyonlara ve global state'e birçok geliştiricinin dokunduğu gerçek kod tabanlarında çok daha zor geliyor

      • Gerçekten iyi geliştiriciler, sistemi zaman içinde bu yöne evriltme becerisine sahip olanlardır. Gerçek dünya kodu dağınıktır ama invariant'lardaki boşlukları kademeli olarak azaltmak ve sonraki geliştiricilerin de invariant'ları fark edip korumasını kolaylaştıran bir kod yapısı kurmak önemlidir. Dokümantasyon yardımcı olur ama deneyimime göre kodun yapısı bundan daha büyük rol oynar

      • Aslında global state'in tehlikeli olmasının belirleyici nedeni tam da bu. Kodun doğruluğunu kanıtlamak için tüm programı bilmen gerekir. Global değişkenleri immutable hale getirmek, fonksiyon argümanı olarak geçirmek ya da state'i saran wrapper class'larla yönetmek işleri kolaylaştırır; böylece sadece o fonksiyonun çağıranlarını net biçimde bilmen yeter. Fonksiyon içinde assertion'larla ek kısıtlar koyarsan kanıtlama zorluğu belirgin biçimde azalır. Zaten birçok programcı bu kararları veriyor ama bunu ispat bilinciyle değil, içgüdüyle yapıyor

      • Birden fazla geliştiricinin yönettiği global state içeren kodu, "kanseri metastaz yapmış" bir hastaya benzetebilirsin. Tedavisi çok daha zordur; şans ve dış koşullara bağlı olarak bazen kurtarılabilir

      • Yazının da dediği gibi, böyle kodlarda hata çıkma olasılığı çok daha yüksek ve bakım kaynaklı yeni hata riski de daha büyük. En baştan ispatlanabilir bir yapıyla yazmanın neden daha doğru yol olduğunu gösteriyor

      • Bu yazı bana, kod yazma biçimimi sürekli yeniden sorgulayıp daha iyi bir yöne doğru çerçevelemeye çalışma halimi hatırlattı. John Carmack gibi geliştiriciler de zaman geçtikçe eski kodlarına bakıp yetersiz buluyor ve giderek daha "iyi" yapma hissi taşıyor mudur diye merak ediyorum

  • Kodun kanıtlanabilir olması gerektiği fikri, Dekker'in 1959'da mutual exclusion problemini çözerken ortaya koyduğu ilk kavramlardan biri. Bununla ilgili ilginç bir anekdot Dijkstra'nın EWD1303 yazısında geçiyor (orijinal bağlantı). Dijkstra'nın sonraki çalışmaları da bu içgörünün devamı olarak görülebilir

  • Doğru bir ispat yazmak gerçekten zor. Program doğrulama da aynı şekilde kolay değil. Bana göre, elde ispat yazmaya kalkmak verimli değil. İlgili dil ve kod tabanı için idiomatic kod yazarsan invariant ya da önkoşul/sonkoşul düşünmen çok gerekmez. R. Pike ve B. W. Kernighan'ın "The Practice of Programming" kitabında vurgulanan "sadelik, açıklık, genellik" pratikte çok büyük etki yaratır. Biraz ilgili ama farklı bir noktadan, competitive programming yaparsan kod doğruluğunu garanti eden teknikleri gerçekten öğrenmeden bir üst seviyeye çıkamazsın

    • Buna katılmıyorum. Yazarın kastettiği şey tam anlamıyla biçimsel ispat değil; daha çok, kendi kodunun hangi mantıksal özellikleri garanti ettiğini, örneğin invariant'ları, mutlaka düşünmek gerektiği. Bu süreç kodu anlamanın ve içerikle ilgili korkuyu aşmanın en iyi yolu

    • Bence burada neden-sonuç ters dönmüş. Probleme dikkatle yaklaşınca sonuçta kod da doğal olarak açık ve temiz oluyor. Mantık net olmalı ki kod tasarımı da net olsun. Ama kodu güzel yazmanın tek başına doğruluğu getireceğine inanmak anlamsız. Elbette kod ne kadar temizse code review gibi süreçlerde hata o kadar azalır. Unutmamak gereken şey, biçimin işlevi takip ettiğidir

    • İspatın en temel fikri, "bunun neden doğru olduğuna dair gerekçe"dir. Bu, ufak hataları önlemekten ziyade, en başta yönün doğru olup olmadığını kontrol etme sürecidir

    • Kodun doğruluğu için, kodu doğru yazmaktan başka hiçbir alternatif yok. Zor da olsa mutlaka doğru yazılmalı

    • İlk paragrafı tersinden okursan, uygun soyutlamalar yani dile ve kod tabanına uygun idiomatic kod program doğrulamayı kolaylaştırır. Doğru soyutlamalarda loop invariant gibi şeyleri ayrıca düşünmene gerek kalmaz; bu yüzden ispat, kodun doğruluğundan doğal olarak çıkar

  • Mutable/immutable olmak da önemli bir özellik. State'i mümkün olduğunca immutable tutarsan, sadece multithreading değil program durumunu akıl yürütme açısından da karmaşıklık azalır

    • Orijinal yazıda zaten bundan bahsediliyor

  • 80'lerde Carnegie Mellon'da lisans öğrencisiyken bu ilkeler bana açıkça öğretilmişti. Sonrasında hayatım boyunca çok faydasını gördüm. Özellikle recursion ile induction'ın eşdeğerliğini öğrendiğim anı hatırlıyorum; o noktadan sonra recursive algoritmalara, "cevap çıkana kadar körlemesine dene" gibi değil, çok daha temiz bir yaklaşımla bakabildim

    • O dersi yakın zamanda aldım; özellikle functional programming ile birlikte düşününce daha da büyük bir aydınlanma yaşadım