Metode formal dan masa depan pemrograman

• Metode formal adalah alat untuk membuktikan apakah perangkat lunak memenuhi sifat yang dimaksud, dan penyebaran agent coding sedang mengubah penilaian biaya-manfaatnya
• Jane Street dulu memandang bahwa, selain beberapa kasus khusus, metode formal memiliki nilai yang rendah dibanding biayanya, tetapi kini sedang membentuk tim khusus
• seL4 membutuhkan 25 orang-tahun untuk memverifikasi 8.700 baris kode C, dan diperlukan sekitar 23 baris pembuktian serta setengah hari kerja per baris kode
• Kode yang dihasilkan agen masih berbeda dari kualitas yang layak dirilis, sehingga metode formal menjadi penting sebagai sarana untuk mengurangi bottleneck verifikasi dan memberi umpan balik yang kuat kepada agen
• Jane Street menilai mereka memiliki ruang untuk mengembangkan OxCaml dan teknik berorientasi pembuktian secara bersamaan karena dapat mengendalikan bahasanya secara mendalam dan memiliki komunitas pemrogram yang siap

---

Metode formal dan masa depan pemrograman

• Selama 25 tahun terakhir, Jane Street telah mengatakan bahwa mereka tidak tertarik pada metode formal di tingkat organisasi, tetapi kini mereka tidak lagi mempertahankan posisi itu
• Mereka sejak lama menghargai kekuatan alat untuk menulis kode yang lebih baik dan lebih dapat diandalkan, dan sistem tipe dianggap sebagai metode formal ringan yang memberi manfaat besar
• Selain kasus khusus, terutama sintesis perangkat keras, mereka menilai metode formal terlalu mahal sehingga tidak cocok untuk sebagian besar perangkat lunak
• seL4 adalah mikrokernel yang diverifikasi secara formal dan merupakan pencapaian penting, tetapi memverifikasi 8.700 baris kode C membutuhkan 25 orang-tahun
  • Diperlukan sekitar 23 baris pembuktian untuk setiap baris kode, dan sekitar setengah hari kerja untuk memverifikasi satu baris
• Untuk kasus seperti mikrokernel yang kritis terhadap keamanan, dengan risiko tinggi dan spesifikasi yang relatif jelas, pendekatan seperti ini bisa bernilai
• Namun, ini tidak cocok untuk sebagian besar perangkat lunak, dan juga terasa tidak cocok untuk perangkat lunak terpenting milik Jane Street
• Munculnya agent coding mengubah penilaian itu, dan skeptisisme terhadap kemungkinan metode formal berubah menjadi antusiasme
• Jane Street sedang membentuk tim metode formal, dengan harapan menjadikannya alat pembangunan perangkat lunak yang berguna secara luas seperti sistem tipe yang canggih

Mengapa berubah pikiran

• Agent coding mengguncang struktur biaya-manfaat lama dari metode formal dalam beberapa cara
• Ini bukan berarti agen bisa sendirian menyusun pembuktian sulit secara bebas, tetapi model sangat membantu dan memungkinkan lebih banyak orang memakai alat tersebut secara produktif
• Karena penggunaan metode formal menjadi lebih mudah daripada sebelumnya, kini layak meninjau ulang perhitungan efektivitas-biaya di masa lalu

• Bottleneck verifikasi menjadi lebih penting

  • Model semakin pandai menulis kode yang berguna, tetapi masih ada jarak besar antara kode yang dihasilkan model dan kode yang benar-benar layak dirilis
  • Model sangat mengesankan dalam mencapai tujuan yang diberikan, tetapi belum cukup kuat untuk mempertahankan atau meningkatkan kualitas codebase selama proses itu
  • Kode buatan agen memang membaik, tetapi cenderung terlalu rumit, memiliki bug aneh dan banyak edge case, serta sering tidak mengikuti invarian inti codebase
  • Manusia harus menghabiskan banyak waktu untuk memverifikasi apakah kode buatan agen sudah cukup berkualitas
  • Metode formal dapat mengurangi beban verifikasi ini dan membuat proses review lebih efisien

• Agen menjadi lebih kuat lewat umpan balik

  • Agen memperoleh manfaat dari umpan balik baik saat dilatih dengan reinforcement learning maupun saat digunakan untuk coding
  • Metode formal dapat menjadi bentuk umpan balik yang kuat untuk meningkatkan kemampuan agen dalam menyelesaikan masalah sulit
  • Pengujian juga sangat bernilai, dan bisa menjadi lebih baik dengan memanfaatkan property-based testing dan fuzzing
  • Namun pengujian saja tidak cukup, dan ada keterbatasan mendasar dalam mencakup ruang keadaan yang dapat dijelajahi program
  • Dalam pengalaman pemrograman OxCaml, agen memperoleh manfaat besar dari jaminan universal yang diberikan sistem tipe
  • Jika sistem tipe bisa mencegah data race, maka data race dapat dihilangkan
  • Jika tipe disusun dengan baik sehingga kerentanan cross-site scripting menjadi mustahil, maka kerentanan itu bisa dihapus dengan cara yang sulit dicapai lewat pengujian biasa
  • Tipe membantu meredakan bottleneck verifikasi dan memberikan umpan balik yang lebih baik saat memrogram bersama agen
  • Memanfaatkan teknik pembuktian yang lebih kuat dapat membuka ruang peningkatan tambahan

Mengapa dilakukan di sini

• Seluruh dunia sedang memikirkan arti agen bagi masa depan pemrograman, dan ada banyak startup yang mencoba menggabungkan metode formal dengan agen
• Jane Street dapat mengendalikan bahasa yang mereka gunakan secara mendalam, sehingga mereka bisa menyesuaikan bahasa itu agar lebih cocok untuk teknik berorientasi pembuktian
• Ada berbagai arah yang mungkin
  • Spesifikasi modular atas properti dapat diintegrasikan ke dalam sistem tipe
  • Kendala tingkat tipe dapat ditambahkan pada elemen seperti ownership dan mutability untuk mempermudah pembuktian tertentu
  • Teknik pembuktian dapat dimasukkan langsung ke dalam bahasa

• Komunitas pemrogram yang siap

  • Jane Street memiliki komunitas pemrogram yang siap menerima teknik-teknik seperti ini
  • Bagi orang yang bekerja pada bahasa pemrograman, sering kali lebih sulit membuat orang benar-benar memakai ide pemrograman yang lebih baik dalam pekerjaan nyata daripada sekadar menciptakan ide itu
  • Di Jane Street, cukup sering ada pengguna yang mengeluh karena fitur sistem tipe baru yang dijanjikan dan tidak biasa tidak hadir cukup cepat
  • Ada banyak orang dengan latar belakang yang bisa memanfaatkan teknik ini, dan perhatian terhadap hasil yang benar serta perangkat lunak berkualitas tinggi juga sudah mengakar
  • Basis pengguna yang aktif dan berekspektasi tinggi memberi kebebasan untuk mencoba perbaikan jangka pendek sekaligus visi jangka panjang
  • Perbaikan jangka pendek dapat memberi dampak relatif cepat
  • Visi jangka panjang menjadi sasaran yang lebih ambisius yang bisa dicapai selama beberapa tahun
  • Sambil belajar dari upaya jangka pendek, mereka dapat membangun menuju tujuan jangka panjang

• Hubungan dengan alat eksternal

  • Mereka tidak mengabaikan pekerjaan dari dunia luar, dan memperoleh harapan serta inspirasi dari karya komunitas berbagai bahasa pemrograman
  • Alat yang relevan mencakup Lean, Dafny, Rocq, Agda, Iris
  • Mereka sedang mencari cara untuk mengintegrasikan OxCaml dengan sebagian alat ini agar bisa memanfaatkan infrastruktur unggulan yang sudah ada
  • Mereka juga menilai ada keunggulan unik yang hanya bisa diwujudkan ketika bahasa dan teknik pembuktian ditangani secara bersamaan

Bergabung

• Jane Street sedang mencari talenta terkait metode formal di London dan New York
• Saat ini, wawancara untuk posisi tersebut dan pembentukan timnya masih berada pada tahap awal
• Masih ada sangat banyak pekerjaan yang harus dilakukan, dan mereka sedang mencari orang untuk bergabung dengan tim

Tambahan

• Model masih memerlukan bantuan dan arahan manusia saat menangani pembuktian yang kompleks
• Pemrogram manusia dapat memiliki gagasan tentang mengapa sistem bekerja dan bagaimana membuktikannya di tingkat tinggi
• Sebagian besar pemrogram tidak tahu cara mengodekan gagasan pembuktian agar memenuhi sistem pembuktian tertentu
• Model dapat mengotomatiskan banyak pekerjaan berulang dalam detail teknis penulisan pembuktian dan menyediakan keahlian di sana
• Celah seperti Obj.magic dapat memungkinkan orang melewati kendala di tingkat tipe
• Jika pengecualian seperti ini dilacak dan dilarang pada sebagian besar kode, maka kondisi yang sangat dekat dengan jaminan universal bisa dicapai
• Metode formal dapat membuat alasan mengapa penggunaan celah seperti ini benar-benar aman menjadi eksplisit

[GN⁺]

Komentar Hacker News

• Beberapa dekade lalu pernah mengerjakan pembuktian kebenaran, dan pada saat itu sistem yang dipakai justru memiliki otomatisasi pembuktian lebih banyak daripada banyak sistem setelahnya
  Bagian yang mudah diselesaikan oleh penyederhana Oppen-Nelson, solver SAT pertama, sedangkan bagian yang sulit ditangani oleh pembukti Boyer-Moore yang menggunakan heuristik dan lemma sebelumnya. Pekerjaan sulit bagi manusia adalah mencoba dengan pembukti lalu mengusulkan lemma yang bisa dipakai pada pembuktian berikutnya
  Sistem-sistem setelahnya tampak memiliki otomatisasi yang lebih sedikit, dan menurut saya alasan metode formal melenceng adalah karena terlalu tenggelam dalam formalisme dibanding kebutuhan praktik. Dari sudut pandang orang yang ingin kode bebas bug dalam proyek komersial, proyek ala akademik terasa terjebak dalam bias matematikawan yang lebih menyukai notasi ringkas untuk makalah dan analisis kasus yang sedikit
  Dalam praktiknya, yang dibutuhkan adalah banyak kerja otomatis yang berat dan sedikit kebutuhan akan insight. Orang-orang pintar terus membuat logika baru seperti modal logic dan temporal logic untuk menghindari panjang lebar pembuktian dengan kertas dan pensil, tetapi itu tidak banyak membantu. Kebenaran dasar di bidang ini adalah bahwa kebanyakan teorema sebenarnya cukup biasa saja
  Seperti kata orang-orang Jane Street, kemampuan untuk mengendalikan bahasa adalah keuntungan besar. Kalimat verifikasi harus terintegrasi ke dalam bahasa pemrograman; jika ditaruh dalam komentar, sintaks lain, atau file terpisah, itu hanya menambah pekerjaan yang tidak perlu. Bagus rasanya melihat Jane Street mendorong arah ini
  Saya mengerjakan ini terlalu dini, lebih dari 40 tahun lalu, dan saat itu membangun teori bilangan dari nol dengan pembukti Boyer-Moore memakan waktu komputasi sekitar 45 menit, tetapi sekarang bahkan tidak sampai 1 detik
  https://archive.org/details/manualzilla-id-5928072/page/n3/m...

  • Sebagai orang yang sudah lama berkecimpung di metode formal, saya agak sulit setuju dengan pernyataan bahwa logika baru tidak membantu. Logika untuk industri itu praktis, dan memungkinkan kita menulis properti canggih yang harus dipenuhi sistem secara sangat ringkas
    Logika menempati posisi dalam ilmu komputer dan rekayasa perangkat lunak yang mirip dengan kalkulus dalam fisika, teknik mesin, dan teknik sipil. Hal-hal seperti LTL atau separation logic yang lebih baru merupakan terobosan besar
    TLA+ yang cukup populer adalah buktinya, dan model checking sangat praktis. Hal yang menarik sekarang adalah apakah metode formal yang lebih berat, terutama theorem proving, bisa menjadi cukup murah untuk dipakai bahkan pada perangkat lunak sistem umum
    Menulis spesifikasi formal untuk fungsi lalu mensintesisnya dan membuktikan kebenarannya dengan hibrida SAT/SMT, theorem prover, dan LLM mungkin akan segera menjadi standar
    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
  • Dalam spesifikasi formal, hal bahwa manusia bisa menafsirkan dan menulisnya akan menjadi sangat penting
    Yang mengkhawatirkan adalah munculnya matematika yang sulit dibaca, lalu dijaga oleh kelompok kecil penganutnya. Notasi-notasi sulit yang berbeda tidak saling kompatibel, dan memahami satu belum tentu banyak membantu untuk memahami yang lain. Kebanyakan orang akhirnya hanya akan menulis kalimat bahasa Inggris yang tidak bisa diverifikasi dengan baik
    Yang lebih buruk, orang bisa saja membiarkan mesin memformalkan kalimatnya sendiri, lalu ikut dalam teater verifikasi tanpa memahami formalisme atau pembuktiannya, dan berpura-pura terkejut saat semuanya meledak
  • Penasaran apakah pernah melihat Ada/SPARK. Kalau iya, saya juga ingin tahu apakah itu sesuai dengan intuisi tentang bagaimana hal ini seharusnya berjalan
    Ada upaya perlahan untuk mengintegrasikan kemampuan semacam ini pada bagian-bagian yang tidak bisa cepat ditangani oleh type system, jadi saya tertarik pada sudut pandang dari orang yang pernah lebih dulu menempuh jalur ini

• Bagus. Dalam beberapa bulan terakhir saya di Scala 3 menggunakan tipe yang ekspresif agar tipe bisa memuat semakin banyak pembuktian waktu kompilasi. Saya tidak memakai macro, meski beberapa tampak layak dipakai
  Pendekatan ini tampaknya bukan hanya membantu mengurangi masalah menjamurnya pengujian ala agen, tetapi juga mencegah agen jatuh ke cara kerja berkualitas rendah. Khususnya, ini mencegah penumpukan nomina ketika agen membuat tipe nominal baru untuk segala hal, bahkan saat seharusnya melakukan generalisasi secara wajar
  Menurut saya, hal yang akan mempercepat agent coding berkualitas adalah alat-alat yang mirip metode formal, termasuk bahasa dengan type system yang kuat
  Yang saya maksud dengan tipe yang ekspresif di sini adalah teknik yang mungkin tidak ingin Anda masukkan ke codebase umum kecuali timnya memang sudah terbiasa dengan type-level programming. Artinya, tim itu harus melihat higher-kinded types dan type functions bukan sebagai hal aneh, melainkan sebagai blok dasar
  Agen, dari sisi pengetahuan, pada umumnya lebih jago “matematika” daripada kebanyakan pengembang, dan sering kali bahkan lebih baik daripada pengembang yang sangat dipengaruhi teori kategori. Ditambah lagi, jika dianggap punya kesabaran “tak terbatas” untuk percakapan, mereka juga cukup bagus untuk mengajar
  Secara pribadi, saya pernah meminta Codex mengubah beberapa pembuktian hobi ke gaya Lean, dan itu sangat mudah. Saya tidak bilang 100% “benar”, dan untuk memeriksa lebih teliti saya masih perlu lebih banyak belajar Lean 4, tetapi pada dasarnya ia tampak memeriksa jebakan pembuktian klasik juga. Saya sangat antusias dengan masa depan metode formal

• Tampaknya ini bicara tentang menggeser nilai manusia ke sisi verifikasi karena Gen AI menghasilkan banyak kode. Kadang saya berpikir tentang apa sebenarnya pemrograman itu.
  Dari sudut pandang orang yang bahasa ibunya bukan bahasa Inggris, mempelajari pemrograman itu sendiri sudah merupakan tantangan besar. Untuk memahami dokumen berbahasa Inggris yang belum diterjemahkan, saya harus bergantung pada terjemahan mesin, dan materi dalam bahasa saya sendiri tertinggal sekitar 5~6 tahun.
  Sekarang, karena mustahil melakukan code review terhadap puluhan ribu baris kode yang dibuat AI, tampaknya muncul pembahasan untuk menetapkan aturan absolut seperti pembuktian matematis. Saat membaca tulisan ini, saya teringat borrow checker di Rust. Dalam praktiknya, setelah beberapa kali memakai Rust, orang sering berakhir mengembangkan kebiasaan buruk berupa trik-trik untuk menghindari borrow checker.
  Kalau ketelitian matematis terlalu berlebihan, orang akan mencari jalan memutar. Programmer yang pendidikannya kurang seperti saya terutama rentan terhadap itu.
  Saya rasa upaya seperti ini pada akhirnya akan menghasilkan penulisan kode yang hanya ditujukan untuk jawaban formal tertentu. Jika nanti jadi terlalu terstandarisasi seperti itu, saya tidak yakin apakah ia masih bisa merespons kebutuhan manusia.
  Upaya pemrograman defensif seperti ini tidak masalah, tetapi dengan istilah buatan saya sendiri, saya ingin melakukan pemrograman agresif. Yaitu pendekatan yang berani mengambil risiko, tetapi cepat memperbaiki dan merilis, sambil percaya bahwa seiring waktu hasilnya akan menjadi cukup baik.
  Tentu saja, di industri mapan seperti Jane Street, di mana akurasi sangat penting dan ruang lingkup pekerjaan terdefinisi dengan baik, pendekatan tulisan ini memang tepat. Itu karena ada cukup data untuk memodelkan kebutuhan pasar dengan layak.
  Tetapi bagi pecundang sosial seperti saya yang terus berpindah mencari tambang emas demi menghasilkan uang, metodologi seperti ini terlihat seperti kemewahan. Bisnis mapan dengan pemodelan yang matang harus terus dioptimalkan oleh tenaga profesional berpendidikan tinggi, dan saya tahu secara realistis tidak mungkin mengejar permintaan itu. Karena itu saya mencari tempat yang pemodelannya belum terstruktur, tetapi saya juga tidak tahu apakah pendekatan ini bisa dipakai di sana.

  • Ini harus dilihat dari sudut pandang Jane Street. Mereka adalah perusahaan perdagangan frekuensi tinggi dan memperdagangkan saham serta instrumen keuangan dalam jutaan, mungkin bahkan puluhan juta unit.
    Di sana tidak ada konsep “nanti tinggal diperbaiki”. Saat Anda memahami apa yang salah, mungkin Anda sudah kehilangan miliaran.
    Jadi pendekatan agresif mungkin hanya cocok di area non-inti.
    Sebagai catatan, pendekatan defensif sebenarnya sudah dipakai di banyak tempat. Python, Java, dan lain-lain punya garbage collector, dan dalam arti tertentu itu memverifikasi bahwa kode berjalan sebagaimana dimaksud.
    Saya memang penasaran kapan verifikasi formal akan mulai terlihat, dan rasanya wajar untuk bergerak dari tahap mengkhawatirkan detail implementasi ke tahap mendeskripsikan masalah secara ilmiah dan matematis.
  • Saya suka istilah “pemrograman agresif”. Hanya saja, paradigma itu sebenarnya sudah menjadi kondisi default industri.
    Karena Gen AI, biaya pemrograman defensif turun drastis, sementara biaya verifikasi manusia naik drastis. Di sisi lain, teknik formal membuat verifikasi menjadi murah, tetapi overhead implementasinya besar karena harus menulis spesifikasi, tipe, bukti, dan membengkokkan implementasi agar sesuai dengan kerangka yang kaku.
    Namun Gen AI bisa mengotomatisasi pekerjaan sulit itu. Keduanya benar-benar pasangan yang serasi.
  • Jika Anda bergantung pada terjemahan mesin untuk dokumen berbahasa Inggris yang belum diterjemahkan, ini memang agak keluar dari topik, tetapi saya sangat menyarankan belajar bahasa Inggris.
    Perlu sedikit usaha, tetapi menghilangkan overhead terjemahan yang terus-menerus akan sangat membantu.
  • Saya setuju bahwa metodologi seperti ini adalah kemewahan. Tulisannya juga mengakui hal itu, dan Jane Street adalah organisasi yang secara khusus sangat siap untuk mendapatkan manfaat dari pendekatan ini.
  • Wajar saja Jane Street menulis hal seperti itu karena memang relevan bagi mereka, dan wajar juga kalau itu tidak berlaku umum untuk semua pemrograman.
    Hanya saja, saya kurang paham bagaimana menyebut diri sendiri “pecundang sosial” atau tidak mengikuti praktik semacam ini dalam karier berhubungan dengan poin argumen tersebut.

• Akhir-akhir ini saya bermain-main dengan ide terkait, dan yang mengejutkan adalah seberapa baik model frontier, khususnya ChatGPT-5.5, menyelesaikan bukti manual tertentu di Roqc, yang dulu merupakan asisten pembuktian Coq.
  Buktinya memang tidak selalu indah, tetapi ChatGPT sering menyelesaikan dalam hitungan menit dan 10~100 iterasi pekerjaan yang bagi saya akan memakan waktu jauh lebih lama, meskipun saya punya pengalaman terbatas tapi bukan nol dengan asisten pembuktian dan pengalaman domain yang cukup besar pada bidang lema yang sedang dibuktikan.
  Dalam konteks tulisan singkat ini, hal ini menarik karena mengguncang asumsi dasar cara kerja alat teknik formal tertentu. Frama-C, Ada/SPARK, dan sebagainya berfokus pada menghasilkan kewajiban pembuktian yang bisa diselesaikan otomatis oleh alat seperti CVC5 dan Z3, dan jika gagal, mereka beralih ke alternatif yang cukup menyakitkan berupa pembuktian manual di Roqc.
  Alur yang umum adalah menemukan bahwa suatu kewajiban itu “sulit”, yaitu tidak terselesaikan secara otomatis, lalu menyusun ulang himpunan lema bantu dan asersi yang terlihat pada titik pembangkitan kewajiban dalam kode agar menjadi “mudah”, atau bahkan mengubah kodenya.
  Itu masuk akal di dunia tempat bukti Roqc berbiaya dua kali lipat. Sulit ditulis manusia, dan biaya pemeliharaannya juga besar ketika kode dan bukti di sekitarnya berubah.
  Tetapi jika bukti Roqc menjadi “penyelesaian otomatis dengan AI di dalam loop”, perbedaan biaya itu hilang. Maka kita bisa menulis bukti seperti menulis kode, menempatkan kejelasan yang mudah dibaca manusia sebagai prioritas nomor satu, dan mengesampingkan optimasi untuk compiler atau prover sampai jauh belakangan. Saya masih belum sepenuhnya mencerna implikasinya, tetapi ini cukup menarik.

  • Ketika persyaratan berubah dan situasinya menjadi tidak bisa dibuktikan, seberapa besar kemungkinan AI akan mengubah kode dan persyaratannya agar bukti lebih mudah dibuat?
    Saya belum pernah menangani bukti, tetapi kadang saya melihat bahwa ketika saya bilang “setelah perubahan ini tes ini gagal”, AI justru mengubah tes itu sendiri alih-alih memperbaiki kode agar lulus baik pada tes lama yang memang saya maksud maupun tes baru.
  • Pengalaman saya mirip, tetapi saya memilih Lean. Itu lebih berkaitan dengan fitur yang ingin saya buat.
    Saya menantikan perkembangannya.
  • Saat Anda mengatakan ChatGPT menyelesaikan bukti Roqc dalam hitungan menit dan 10~100 iterasi, saya penasaran bagaimana Anda tahu bahwa bukti itu sendiri benar.

• Setiap kali membaca tentang spesifikasi formal, rasanya seperti “menulis pengujian yang sama dengan cara berbeda”, atau lebih buruk lagi seperti “menulis implementasi yang sama dengan cara berbeda”
  Menulis dua kali mungkin bisa membantu menangkap kesalahan, tetapi jika spesifikasi formal juga bisa memiliki bug yang sama seperti pengujian atau implementasi, saya kurang paham apa yang membuatnya istimewa
  Masalah dasarnya adalah, untuk membuktikan secara formal bahwa sebuah program melakukan sesuatu, kita harus mendefinisikan “sesuatu” itu dengan sangat spesifik. Pada akhirnya itu terasa seperti menulis ulang pengujian atau implementasi
  Saya sudah sesekali melihat topik ini selama beberapa tahun, dan terus merasa ada sesuatu yang saya lewatkan, tapi saya tidak tahu apa itu. Adakah yang bisa menjelaskannya?

  • Seperti kutipan terkenal dari Dijkstra, “pengujian program dapat menunjukkan adanya bug, tetapi tidak dapat menunjukkan ketiadaannya”
    Kekurangan pengujian adalah kita hanya bisa menguji perilaku yang kita anggap mungkin menjadi masalah. Untuk secara proaktif memperbaiki perilaku yang bahkan tidak kita sadari bisa salah, kita memerlukan alat yang lebih tidak biasa di kotak peralatan kita. Fuzz testing adalah salah satu awal ke arah itu, dan verifikasi formal adalah awal lainnya
    Tentu saja, kualitas alat seperti ini bergantung pada seberapa baik kita menulis model formal yang komprehensif yang mengizinkan perilaku yang diinginkan dan melarang perilaku yang tidak diinginkan, dan di banyak bidang kita masih sangat jauh dari titik itu
  • Perbedaan besarnya adalah bahwa metode formal memungkinkan kita memakai kuantor universal untuk semua hal
    Misalnya, dalam unit test kita bisa menulis “foo('abc') mengembalikan string tanpa spasi di akhir”
    Tetapi dengan metode formal, kita bisa membuktikan “untuk sembarang input x, foo(x) mengembalikan string tanpa spasi di akhir”
    Ini contoh yang sepele, tetapi kita juga bisa membayangkan hal yang lebih kompleks seperti “untuk sembarang program P, compile(P) berperilaku sama dengan P”
    Tentu saja, kita tetap harus mendefinisikan apa yang dimaksud dengan “berperilaku sama”
  • Saya tidak menggunakannya untuk perangkat lunak, tetapi dalam desain ASIC dan FPGA, spesifikasi metode formal memungkinkan alat seperti SAT solver menentukan apakah desain target memenuhi spesifikasi
    Anda menetapkan properti desain, lalu alat tersebut menguji desain dengan berbagai cara untuk memeriksa apakah properti itu bisa dilanggar
    Misalnya, untuk sistem yang mengendalikan lampu lalu lintas, Anda bisa menetapkan properti bahwa lajur yang saling berpotongan tidak boleh sama-sama hijau pada saat yang sama, atau dalam selang waktu tertentu
    Alat itu dapat memeriksanya dengan pencarian menyeluruh dan menunjukkan jejak kode yang melanggarnya
  • Ini lebih dari sekadar “menulis pengujian yang sama dengan cara berbeda”. Setiap pengujian umumnya berdiri sendiri atau membesar hingga tak lagi bisa dikelola, dan kelengkapan sekumpulan pengujian biasanya harus dinilai lewat tumpang tindih yang relatif kasar seperti branch coverage
    Sistem tipe yang dibuktikan secara statis memungkinkan setiap komponen diperiksa agar cocok dengan semua komponen lain sebelumnya. Bukan sekadar “pengujian ini lolos”, tetapi menjamin bahwa ketika digabungkan, “semua pengujian ini membentuk keseluruhan yang masuk akal dan konsisten”, serta mencegah model yang tidak konsisten diimplementasikan ke dalam kode
    Ini mirip seperti memperluas persyaratan match di Rust agar mencakup semua cabang yang mungkin, tetapi pada skala seluruh codebase
    Memang benar bahwa ini tidak akan menangkap kesalahan logika atau teori yang mendasar. Tetapi Anda mungkin akan terkejut betapa jauh lebih kokohnya ini dibanding misalnya gabungan sistem tipe Haskell, pengujian fungsional ad hoc, dan property testing. Semua itu juga merupakan sistem yang kuat secara keseluruhan, tetapi kriptografi yang dibuktikan secara formal menetapkan standar yang jauh lebih tinggi
  • Perbedaan yang kuat ada antara pengujian tertentu dan pembuktian menyeluruh. Jika Anda tidak terpikir untuk menguji kondisi batas, itu akan terlewat begitu saja. Jika modelnya bagus, Anda bisa mengetahui keberadaannya dan memperbaikinya sebelum rilis
    Ini sangat bernilai terutama dalam situasi konkuren, terdistribusi, dan multi-threaded. Race condition dan deadlock sangat sulit diuji dan ditalar, dan persoalan seperti “bisakah A, B, C terjadi dalam urutan A, C, B” adalah contohnya
    Kematangan bidang ini tampaknya akan berkembang kira-kira seperti ini. Pertama, LLM pada awalnya mungkin hanya sampai pada verifikasi pasca-hoc bergaya “mencoba untuk kedua kalinya”, tetapi akan sangat mempercepat pembelajaran dan penggunaan metode formal
    Kedua, ini akan bergerak ke arah otomasi di mana LLM memeriksa “kode implementasi berubah, apakah tampaknya modelnya rusak?” Ini tetap tidak deterministik, tetapi kemungkinan jauh lebih baik daripada manusia harus me-review sesuatu yang hanya sesekali berubah
    Ketiga, lompatan yang sesungguhnya akan ada pada membawa alat “tulis spesifikasi formal saja, lalu hasilkan implementasinya” ke tahap berikutnya. Sudah ada banyak proyek pembangkitan kode seperti ini, tetapi sebagian besar belum benar-benar matang sampai tingkat yang diinginkan perusahaan. Bagaimana jika alat LLM bisa mempercepat 1–2 tahun kerja manual yang diperlukan untuk menyesuaikan salah satunya dengan kebutuhan?

• Tulisan Kleppmann sebelumnya https://martin.kleppmann.com/2025/12/08/ai-formal-verificati... juga layak dilihat, dan tentu saja kita perlu menimbang apakah hal-hal yang bisa dimasukkan ke type system atau linter sebaiknya memang dimasukkan ke sana
  Saya berharap muncul cara yang lebih mudah digunakan. Dari alat yang disebut dalam tulisan itu, dafny dan iris tampaknya paling dekat ke penggunaan industri. Saya juga tahu Amazon S3 punya riwayat menggunakan TLA secara internal
  Tetapi saya rasa saya masih belum melihat padanan TypeScript untuk bidang ini: sesuatu yang masuk secara alami ke alat yang sudah ada, bekerja seperti abstraksi tanpa biaya, dan sungguh-sungguh lebih disukai orang daripada cara lama
  Bahkan memakai linter kustom pun masih terasa cukup buruk. golangci-lint adalah codebase yang menyakitkan, dan saya belum pernah memakai semgrep, tetapi mesin aturannya terlihat mengintimidasi. Saya juga belum pernah memakai AST API yang benar-benar saya sukai

• Pujian terhadap penalaran deduktif, yaitu “metode formal”, seperti ini selalu melewatkan keterbatasan dasarnya. Masalahnya adalah seberapa baik aksioma dan definisi cocok dengan domain sasaran
  Ini seperti ungkapan, “Secara teori tidak ada perbedaan antara teori dan praktik. Dalam praktiknya…” Saya menduga Jane Street akan tetap memelihara codebase besar dengan pemetaan 1:1 karena tujuan kodenya adalah mengimplementasikan algoritme deterministik. Banyak pengembang memang bekerja di area seperti itu, tetapi jutaan lainnya tidak. Sebagian besar UI, sebagian besar pekerjaan eksploratif, dan sebagainya termasuk di sini
  Di samping metode formal, ada juga arus yang berusaha mendefinisikan kriteria persetujuan dengan resolusi tinggi, meski bukan dengan pendekatan logika atau matematika. Arus ini setidaknya bergulat dengan masalah pemetaan, tetapi di sebagian besar tempat, di mana peta bukanlah wilayahnya, itu tidak menyelesaikannya
  Halaman hasil pencarian Google punya framework optimasi internal yang sangat berkembang, tetapi apakah itu benar-benar sudah mencapai titik optimum? Mungkinkah prototipe yang dibuat tergesa-gesa untuk menangkap ide yang masih samar justru bisa menunjukkan sesuatu yang lebih baik? Pertanyaan seperti ini paling baik dijawab dengan melihat ke luar yang dilayani sistem itu, bukan ke dalam sistemnya sendiri

  • Metode formal memang tepat untuk domain yang semantiknya terdefinisi dengan baik
    Rangkaian logika, komponen CPU yang banyak memakai verifikasi formal, kernel, protokol, parser, compiler, kriptografi, framework keamanan, primitive konkurensi, dan sebagainya mendapat manfaat besar dari verifikasi
  • Kebanyakan UI di dunia nyata pada akhirnya bermuara pada state machine, dan ini sangat cocok untuk verifikasi formal
    Jika ingin belajar lebih jauh, tulisan Hillel Wayne adalah titik awal yang bagus: https://www.hillelwayne.com/formally-specifying-uis/
  • Halaman hasil Google itu sendiri tidak terdefinisi dengan baik, tetapi mungkin lebih dari 90% kode di bawahnya terdefinisi dengan baik
    Dan dalam beberapa kasus, hasilnya bisa dipelajari meskipun tidak terdefinisi dengan baik, jadi ini bukan semata-mata soal duduk dan memikirkan apa yang masuk akal

• Dari sudut pandang seseorang yang agak tertarik pada desain dan implementasi bahasa pemrograman, kalimat ini benar-benar menarik. “Bagi kebanyakan orang yang bekerja dengan bahasa pemrograman, bagian yang mudah adalah menghasilkan ide-ide baru dan lebih baik untuk membuat pemrograman menjadi lebih baik. Bagian yang sulit adalah meyakinkan seseorang untuk memakai ide itu dalam pekerjaan nyata”
  Saya sepenuhnya setuju. Bahkan jika ada manfaatnya, ada batas pada seberapa banyak keasingan yang bisa dimasukkan ke bahasa baru
  Namun, agen AI tampaknya tidak akan merasakan resistansi besar terhadap ide-ide yang secara radikal baru dalam desain bahasa pemrograman. Saya sudah cukup lama memikirkan bagaimana desain bahasa pemrograman akan berevolusi setelah AI agentic
  Akan sangat menarik melihat ide-ide baru apa yang bisa diciptakan untuk memperbaiki bahasa pemrograman ketika kita jauh lebih sedikit perlu khawatir soal adopsi
  https://steveklabnik.com/writing/the-language-strangeness-bu...

• Saya sedang mengerjakan penerapan metode formal di bidang application security testing, dan saya melihat pendekatan yang sama juga bisa diterapkan pada verifikasi business logic
  Untuk itu saya memakai taint analysis. Ini pendekatan metode formal yang cukup mapan, tetapi di lapangan masih belum diterapkan secara luas karena kompleksitas aliran data di codebase nyata
  Memperluas metode formal melampaui AST pattern matching dan type checking sederhana adalah pekerjaan yang benar-benar sulit. Butuh R&D bertahun-tahun sampai taint analysis bisa mencapai level mampu melacak aliran data antarprosedur dalam codebase nyata dalam hitungan menit dan menemukan kerentanan yang tersembunyi dalam
  Jika tertarik, bisa melihat proyeknya: https://github.com/seqra/opentaint

• Sekitar 18 bulan lalu saya mulai tergila-gila memakai tipe bersama LLM, dan saya mulai serius dengan lean4 kira-kira 6–8 bulan lalu. Sekarang saya bahkan tidak mempertimbangkan memakai bantuan AI untuk pekerjaan perangkat lunak tanpa basis pembuktian CIC dengan FFI C/C++ yang praktis, yang berarti pada dasarnya bisa terhubung ke segalanya
  Dari JSON sampai Python semuanya saya larang, dan nix pun saya tulis ulang agar ada compiler-nya. Hampir semua yang kami gunakan bukan hanya diuji sampai batasnya dengan property testing dan berbagai fuzz test, tetapi juga memiliki pembuktian lean4 yang setidaknya menjalankan property test melalui tautan .olean. Jika ada waktu luang, kami bahkan membuktikan kelengkapan seluruh domain dan menguji properti itu juga
  Semua bagian yang cepat dihasilkan dari lean4, jadi saya melewati perdebatan C++/Rust. Ada keuntungan saat bug di C++ ternyata sebenarnya bug di kode lean4, tetapi bisa mengarah ke dua-duanya
  Ini perubahan besar, dan saya tidak menyalahkan orang yang skeptis dan berkata, “Melarang JSON dan Python?” Tetapi kami sudah memeriksa jutaan baris dengan cara ini, dan AI + sistem formal adalah lompatan yang jauh lebih besar daripada beralih dari tanpa AI ke AI dan Python. Yang belakangan, menurut pengalaman kami, kemajuannya tidak monoton, sedangkan yang pertama hampir selalu bergerak maju secara monoton
  Hal yang cukup berani juga dimungkinkan. Ini adalah pembuktian formal atas komputasi tensor poliedral yang dimodelkan oleh hal-hal seperti ISL dan CuTe, dan dengan itu Anda bisa melakukan swizzling dan tiling pada perangkat dengan mdspan milik C++23 dan sekaligus membuktikan bahwa itu benar. Namun contoh ini tidak terlalu menunjukkan argumen ala L'Hopital tentang cakupan: https://github.com/b7r6/mdspan-cute
  Hasilnya benar-benar cepat, dan cepat sejak percobaan pertama
  https://straylight.software/assets/lambda-hierarchy.svg

  • Menempatkan Agda dan Idris 2 di bawah CIC membuat diagram hierarki lambda itu, bahkan jika dinilai baik-baik, menjadi menyesatkan
  • Jadi saya penasaran perangkat lunak apa yang dibuat, dan mengapa itu berguna