Cara Menjadi Programmer yang Lebih Baik dengan Membuat Pembuktian Kecil di Dalam Kepala

• Untuk menjadi programmer yang lebih baik, penting membangun kebiasaan menggambar pembuktian kecil di dalam kepala saat menulis kode
• Monotonisitas, imutabilitas, pre-condition dan post-condition, serta invariant adalah konsep inti saat melakukan pembuktian mini seperti ini
• Merancang dengan mempertimbangkan cakupan dampak perubahan kode terhadap seluruh sistem (isolasi, firewall) sangat membantu mengurangi kompleksitas dan risiko
• Dengan memanfaatkan induksi, kita dapat membuktikan kebenaran fungsi atau struktur rekursif secara bertahap
• Pola pikir ini dibangun lewat latihan dan pembiasaan, dan latihan pembuktian matematis serta pemecahan soal algoritme sangat membantu

---

Pengantar dan gagasan inti

• Penulis, seiring bertambahnya pengalaman, secara alami membentuk kebiasaan ‘membayangkan pembuktian kecil’ untuk meningkatkan ketepatan dan kecepatan kode
• Proses memverifikasi dan menalar perilaku yang diharapkan saat coding di dalam kepala memerlukan latihan, dan ketika sudah mahir, kualitas akhir kode meningkat secara nyata
• Yang penting bukan tepat bagaimana melakukannya, melainkan berlatih dengan berbagai cara yang paling cocok untuk diri sendiri

Monotonisitas (Monotonicity)

• Monotonisitas (monotonicity) berarti sifat fungsi atau kode yang hanya bergerak ke satu arah
• Contohnya adalah checkpointing, di mana tahapan pekerjaan hanya maju ke depan, dan pekerjaan yang sudah selesai tidak kembali dijalankan dari belakang
• Dalam contoh LSM tree yang dibandingkan dengan B-tree, LSM tree umumnya memiliki karakteristik ruang yang terus terakumulasi dan hanya berkurang saat proses compaction
• Jika monotonisitas terjamin, kita bisa secara alami menyingkirkan atau memprediksi sebagian state atau hasil yang kompleks
• Imutabilitas (immutability) juga merupakan konsep serupa, karena nilai yang sekali ditetapkan tidak akan pernah berubah, sehingga kemungkinan perubahan state bisa dikesampingkan

Pre-condition dan post-condition

• Pre-condition dan post-condition adalah pernyataan yang harus selalu benar sebelum dan sesudah sebuah fungsi dijalankan
• Melacak kondisi ini secara eksplisit saat menulis fungsi membantu penalaran logis dan pengujian
• Jika post-condition didefinisikan dengan jelas, kasus uji unit test bisa diturunkan dengan lebih mudah
• Menambahkan assertion ke dalam kode untuk memverifikasi kondisi-kondisi ini agar eksekusi berhenti lebih awal dalam situasi tak terduga akan meningkatkan prediktabilitas dan keamanan
• Ada juga kasus ketika sulit memberikan pre-condition/post-condition yang jelas pada sebuah fungsi, dan menemukan hal itu sendiri pun memberi wawasan penting

Invariant

• Invariant adalah sifat yang harus selalu benar dalam kondisi apa pun, sebelum, selama, dan sesudah eksekusi kode
• Contoh invariant yang representatif adalah persamaan akuntansi dalam pembukuan berpasangan (total kredit = total debit)
• Jika seluruh kode dipecah menjadi langkah-langkah kecil, lalu dibuktikan bahwa setiap langkah mempertahankan invariant, maka integritas keseluruhan bisa dijaga
• Ada pendekatan menggunakan listener atau lifecycle method untuk menjaga invariant (misalnya constructor/destructor di C++, useEffect di React, dan sebagainya)
• Verifikasi invariant jauh lebih mudah ketika perubahan sedikit atau jalurnya sederhana

Isolasi (Isolation)

• Salah satu inti dari software yang baik adalah menambah atau mengubah fitur baru tanpa membuat sistem yang sudah ada menjadi tidak stabil
• Kita perlu memahami ‘radius dampak’ (blast radius) dari perubahan kode, lalu membuat ‘firewall’ struktural untuk meminimalkan penyebaran dampaknya
• Melalui contoh layanan nyata Nerve, diperkenalkan pendekatan untuk menetapkan batas yang jelas antara query planner dan query executor, lalu merancang agar bagian yang diubah tidak melintasi batas tersebut
• Mencegah propagasi perubahan yang tidak perlu membuat verifikasi dan maintenance lebih mudah, sekaligus meningkatkan stabilitas
• Ini juga sejalan dengan filosofi OCP (Open-Closed Principle), yaitu memperluas fungsi tanpa mengubah perilaku yang sudah ada

Induksi (Induction)

• Banyak program mencakup fungsi rekursif atau struktur rekursif, dan induksi sangat kuat digunakan saat membangun logika untuk itu
• Untuk membuktikan perilaku dan kebenaran fungsi rekursif secara bertahap, kita perlu memverifikasi kasus dasar (base case) dan langkah induktif (inductive step)
• Contohnya adalah proses penyederhanaan node pada struktur AST (syntax tree), di mana argumentasi induktif di setiap tahap digunakan untuk membuktikan terjaganya invariant dan kebenaran perilaku
• Ketika cara berpikir induktif sudah terinternalisasi, menulis dan memverifikasi kode rekursif menjadi jauh lebih intuitif dan mudah
• Dibandingkan dengan upaya verifikasi global (holistic) yang non-induktif, menarik untuk direnungkan pendekatan mana yang terasa lebih alami

Proof-affinity sebagai metrik kualitas

• Penulis mengajukan gagasan bahwa kode yang memungkinkan kita membayangkan pembuktian kecil di dalam kepala adalah kode yang baik
• Jika kode memiliki struktur seperti monotonisitas, imutabilitas, kondisi yang jelas, pemisahan invariant, batas firewall, dan penggunaan induksi, maka kode itu benar-benar lebih mudah dibuktikan, dan karena itu kualitasnya juga lebih tinggi
• Jika kode sulit dipahami dan sulit diverifikasi, itu menandakan perlunya refactoring atau peninjauan ulang struktur
• Dalam konteks ini, penulis mengusulkan istilah ‘proof-affinity’ alih-alih ‘provability’
• Proof-affinity bukan satu-satunya unsur kualitas software, tetapi merupakan pendorong yang sangat penting bagi pemahaman, pengembangan, pengujian, dan pemeliharaan kode

Cara meningkatkan kemampuan

• Pola pikir logis seperti ini harus dilatih terus hingga dapat diterapkan secara alami tanpa sadar
• Sering menulis pembuktian (matematis) dan melatih kemampuan penalaran logis adalah hal yang esensial
• Pemecahan soal algoritme (kuliah EdX Stanford, Leetcode, dan lain-lain) juga merupakan tempat latihan yang baik; hasil akan lebih baik jika berfokus pada soal yang menuntut implementasi teliti dan cara berpikir pembuktian, bukan sekadar trik
• Daripada berkali-kali memperbaiki hasil sampai benar, lebih penting berlatih untuk mendekati jawaban benar sejak percobaan pertama
• Melalui pembiasaan seperti ini, desain sistem yang logis dan kualitas kode dapat meningkat secara signifikan

[GN⁺]

Komentar Hacker News

• Ada contoh yang sangat pas untuk topik ini, sederhana tetapi mengejutkan: binary search. Ada variasi kiri dan kanan juga, tetapi sangat sulit mengimplementasikannya dengan benar jika tidak memikirkan loop invariant. Tulisan ini menjelaskan pendekatan berbasis invariant dan contoh kode Python yang sesuai. Jon Bentley, penulis Programming Pearls, pernah meminta para programmer IBM mengimplementasikan binary search biasa, dan 90% hasilnya mengandung bug. Kebanyakan kesalahannya berupa terjebak dalam loop tak berujung. Pada masa itu integer overflow juga harus ditangani sendiri, jadi sampai batas tertentu bisa dimengerti, tetapi tetap saja persentasenya mengejutkan

  • Setelah melihat ini, saya mulai memakai binary search sebagai pertanyaan wawancara. Sekitar 2/3 kandidat yang dikenal bagus tidak bisa membuat implementasi yang benar-benar berjalan dengan benar dalam waktu 20 menit. Terutama, banyak yang terjebak dalam loop tak berujung pada kasus yang mudah. Orang-orang yang berhasil biasanya mengimplementasikannya dengan cepat. Salah satu penyebabnya adalah banyak yang belajar dengan antarmuka yang keliru. Penjelasan Wikipedia juga mengatakan "inisialisasi L ke 0 dan R ke n-1", yang berarti rentangnya inklusif terhadap R. Padahal dalam praktik, untuk kebanyakan algoritma string, bentuk dengan batas atas eksklusif, yakni R = n, lebih baik. Saya ingin menguji hipotesis ini secara langsung. Saya ingin meminta banyak orang menulisnya dengan function prototype dan nilai awal yang berbeda-beda, lalu membandingkan seberapa sering bug muncul saat memakai batas atas inklusif, eksklusif, atau pendekatan berbasis length

  • Memang, binary search adalah contoh yang nyaris paling terkenal untuk sulitnya mengelola indeks. Bersama algoritma partisi Hoare, ini adalah salah satu algoritma dasar yang paling sulit ditulis dengan tepat tanpa kesalahan

  • Sebagai percobaan, saya meminta Claude Sonnet menulis kode Python binary search tanpa bug

  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
  

  Saya juga memeriksa berbagai test case dengan array contoh

  • Mengetahui bahwa bug binary search terkenal sebagai contoh praktik terbaik yang salah, saya pernah menantang diri untuk memasukkan implementasi pertamanya yang bebas bug ke dalam sebuah buku. Saya menulisnya dengan sangat hati-hati, tetapi tetap saja ada bug, jadi cukup lucu. Untungnya, berkat sistem umpan balik awal dari Manning, saya bisa memperbaikinya sebelum dicetak

  • Saya selalu mengimplementasikan binary search kiri/kanan dengan mengingat "nilai terbaik sejauh ini". Mirip dengan cara kerja lower_bound dan upper_bound di C++. Dalam struktur while (l < r), saya mencari titik tengah, memeriksa posisi saat ini, lalu menyesuaikan rentang dengan semestinya. Misalnya untuk upper_bound saya menaikkan batas kiri, dan untuk lower_bound saya menurunkan batas kanan. Sudah lama tidak mengerjakan leetcode, jadi kepala saya agak blank dan formatnya mungkin berantakan

• Sepertinya saya pernah mengenal konsep yang mirip seperti ini dulu di kelas pascasarjana. Sejak sekitar akhir masa sarjana, saya mengerjakan ujian matematika hanya dengan pulpen. Saya sendiri tidak tahu pasti alasannya, tetapi nilai saya selalu tinggi, karena saya menyelesaikannya sekaligus sambil menggambar seluruh alur penyelesaiannya secara utuh di kepala. Berkat itu, kesalahan saya jauh berkurang. Saat menulis kode pun saya memulai dengan cara serupa, setelah merancangnya cukup matang di dalam kepala

• Untuk menjadi programmer yang lebih baik, kita perlu membiasakan diri menulis pembuktian kecil pada kode Test dan definisi tipe adalah contoh langsung dari tindakan itu Khususnya, saya mendekatinya dengan urutan test dulu, lalu tipe, dan terakhir kode Sebaiknya buat test untuk tiap acceptance criteria, dan tulis test yang menjelaskan input/output dengan jelas Kalau berupa API, kita bisa lebih dulu membuat spesifikasi lengkap dengan OpenAPI atau GraphQL, termasuk semua properti dan tipe. Berdasarkan spesifikasi ini, validasi data bisa dilakukan saat runtime, dan spesifikasi itu sendiri menjadi bukti bahwa aplikasi bekerja sesuai spesifikasi Singkatnya, penting untuk memperoleh bukti bahwa sistem benar-benar berjalan sesuai maksud melalui OpenAPI/GraphQL, test, dan tipe Kalau spesifikasinya sendiri dirancang dengan baik sejak awal, implementasi kode bisa diubah secara fleksibel sambil tetap membuktikan kebenarannya lewat spesifikasi Spesifikasi lebih penting daripada kode itu sendiri

  • Lima properti yang disebut dalam tulisan itu bisa diekspresikan dalam type system yang baik. Dengan pendekatan seperti ini, sebagian besar spesifikasi menjadi kode, dan compiler menjamin kebenarannya. Masa depan pemrograman seharusnya bergerak ke arah di mana pendekatan ini menjadi hal yang wajar OpenAPI dan type system GraphQL terlalu miskin, jadi untuk mencapai masa depan seperti itu, kita mungkin masih butuh 50 tahun perkembangan lagi

• Saya belajar dasar-dasar ilmu komputer teoretis di universitas, dan setuju dengan arah tulisan ini. Mempraktikkannya memang tidak mudah Selain precondition/postcondition, teknik pembuktian CS seperti loop invariant dan structural induction juga sangat kuat Saya merekomendasikan tautan loop invariant, structural induction, beserta catatan kuliah UofT CSC236H (catatan kuliah)

  • Catatan kuliah CSC236 ini sangat bagus, dan Profesor David Liu juga orang yang sangat baik profil dosen

  • Wah, UofT disebut! Senang sekali melihatnya

• Gagasan "membuat pembuktian kecil di kepala tentang kode" adalah prinsip yang begitu penting sampai seharusnya terasa jelas dengan sendirinya. Kita harus selalu sadar akan proposisi sederhana tentang apa yang dilakukan setiap bagian kode

  • Semangat ini mudah diterapkan pada proyek greenfield, ketika baru-baru ini kita menulis semua kodenya sendiri, tetapi terasa jauh lebih sulit di codebase nyata, tempat banyak developer menyentuh berbagai fungsi atau global state

    • Developer yang benar-benar hebat mampu mengembangkan sistem sedikit demi sedikit ke arah seperti ini. Kode dunia nyata memang berantakan, tetapi yang penting adalah secara bertahap mengurangi celah dalam invariant, dan membuat struktur kode yang membantu developer berikutnya tetap sadar akan invariant itu serta mendukung pemeliharaannya. Dokumentasi membantu, tetapi menurut pengalaman saya, struktur kode itu sendiri berperan lebih besar

    • Sebenarnya inilah alasan paling berbahaya mengapa global state itu berisiko. Untuk membuktikan kebenaran kode, kita harus mengetahui keseluruhan program. Kalau variabel global diubah menjadi immutable value, diteruskan sebagai argumen fungsi, atau dikelola lewat wrapper class yang membungkus state, maka kita cukup memahami dengan jelas siapa pemanggil fungsi itu. Jika kita menambahkan lebih banyak batasan di dalam fungsi, misalnya lewat assertion, tingkat kesulitan pembuktiannya jelas menurun. Banyak programmer sebenarnya sudah membuat keputusan seperti ini, hanya saja mereka melakukannya secara naluriah tanpa sadar sedang memikirkan pembuktian

    • Kode yang global state-nya dikelola oleh banyak developer bisa dianalogikan seperti pasien dengan "kanker yang telah bermetastasis". Jauh lebih sulit diobati, dan kadang hanya bisa diselamatkan tergantung keberuntungan dan kondisi eksternal

    • Seperti dikatakan artikel itu, kode semacam ini jauh lebih mungkin mengandung bug, dan juga lebih rentan menimbulkan bug tambahan saat dipelihara. Ini menunjukkan bahwa menulis dengan struktur yang bisa dibuktikan sejak awal adalah jalan yang jauh lebih benar

    • Membaca tulisan ini mengingatkan saya pada diri sendiri yang terus-menerus meninjau ulang cara saya menulis kode dan berusaha menata ulang arah yang lebih baik. Saya jadi penasaran apakah developer seperti John Carmack juga, seiring waktu, merasa kode lamanya kurang baik dan punya semacam intuisi untuk terus melakukannya dengan lebih "baik"

• Gagasan bahwa kode harus bisa dibuktikan pertama kali tampak saat Dekker menyelesaikan masalah mutual exclusion pada 1959. Ada anekdot menarik tentang ini dalam tulisan Dijkstra EWD1303 (tautan asli). Riset lanjutan Dijkstra juga bisa dilihat sebagai kelanjutan dari wawasan ini

• Menulis pembuktian yang benar itu sangat sulit. Verifikasi program juga tidak mudah. Menurut saya, mencoba membuat pembuktian manual itu tidak efisien. Jika kita menulis kode yang idiomatis sesuai bahasa dan codebase yang digunakan, biasanya kita tidak terlalu perlu memikirkan invariant atau precondition/postcondition. Penekanan pada "simplicity, clarity, generality" dalam "The Practice of Programming" karya R. Pike dan B. W. Kernighan sangat efektif dalam praktik. Sedikit terkait tetapi topiknya lain, kalau mencoba competitive programming, kita pasti harus benar-benar menguasai teknik untuk menjamin kebenaran kode agar bisa naik ke tingkat berikutnya

  • Saya tidak setuju dengan ini. Menurut saya, yang dimaksud penulis bukanlah pembuktian formal penuh, melainkan bahwa Anda harus benar-benar memikirkan properti logis apa yang dijamin oleh kode Anda, misalnya invariant. Proses ini adalah jalan terbaik untuk memahami kode dan menghilangkan rasa takut terhadap isinya

  • Di sini justru tampaknya sebab dan akibat tertukar. Jika kita mendekati masalah dengan memikirkannya secara hati-hati, hasilnya kode juga akan menjadi jelas dan rapi secara alami. Logika harus jelas agar desain kodenya juga jelas. Tetapi mempercayai bahwa menulis kode dengan cantik akan otomatis membuatnya benar adalah omong kosong. Tentu, makin rapi kodenya, makin sedikit bug dalam code review dan sebagainya. Yang perlu diingat adalah bahwa bentuk mengikuti fungsi

  • Konsep paling dasar dari pembuktian adalah "alasan mengapa ini benar". Ini bukan sekadar untuk mencegah kesalahan kecil, melainkan proses untuk memastikan bahwa arah dasarnya memang benar

  • Untuk ketepatan kode, tidak ada metode pengganti selain menulis kode dengan benar. Sesulit apa pun, pada akhirnya tetap harus ditulis dengan benar

  • Jika paragraf pertama dibalik sepenuhnya, maka dengan abstraksi yang tepat, yakni kode idiomatis yang sesuai dengan bahasa dan codebase, verifikasi program justru menjadi lebih mudah. Karena dalam abstraksi yang tepat kita tidak perlu memikirkan loop invariant dan hal serupa, pembuktian mengikuti langsung dari kebenaran kode

• Mutability dan immutability juga merupakan properti penting. Jika state dibuat immutable sebisa mungkin, kompleksitas berkurang bukan hanya dalam multithreading, tetapi juga saat menalar state program

  • Isi seperti itu sebenarnya sudah ada dalam artikel aslinya

• Pada 1980-an, saat masih mahasiswa sarjana di Carnegie Mellon, saya diajari prinsip-prinsip seperti ini dengan sangat jelas. Setelah itu, ini sangat membantu sepanjang hidup saya. Terutama saat saya belajar kesetaraan antara rekursi dan induksi, saya ingat akhirnya bisa mendekati algoritma rekursif dengan rapi, bukan sekadar "coba-coba sampai dapat jawaban"

  • Saya baru-baru ini mengikuti kuliah itu, dan saat belajar functional programming saya mendapat pencerahan yang lebih besar lagi