Jane Street Mulai Investasi Formal Methods untuk Masa Depan Coding
Judul asli: Formal methods and the future of programming
Mengapa Ini Penting
Menandai perubahan industri dalam adopsi formal methods dengan dukungan AI untuk development yang lebih reliable
Jane Street mengubah sikap setelah 25 tahun menolak formal methods. Perusahaan kini membangun tim khusus karena AI coding agents mengubah perhitungan biaya-manfaat penggunaan formal methods dalam pengembangan software.
Selama 25 tahun, Jane Street menghindari formal methods karena biaya tinggi. Contohnya, verifikasi microkernel seL4 membutuhkan 25 person-years untuk 8.700 baris kode C, dengan 23 baris proof per baris kode. Namun kemunculan agentic coding mengubah perspektif mereka. Yaron Minsky menjelaskan bahwa AI models memudahkan penggunaan formal methods dan memperluas aksesibilitas tools tersebut. Manfaatnya juga meningkat karena dua alasan: pertama, verification bottleneck menjadi lebih penting saat models menghasilkan code yang perlu verifikasi ekstensif; kedua, agents berkembang dengan feedback yang bisa diperkuat formal methods. Jane Street kini membangun tim formal methods dengan harapan menjadikannya tools yang berguna seperti type systems saat ini.