Kesalahan seperti apa yang merupakan kekeliruan sepele

Kesalahan seperti apa yang merupakan kekeliruan sepele

Poin utama

1. Jika suatu kesalahan dalam definisi atau pembuktian mudah diperbaiki tetapi sulit disadari, maka kesalahan itu bukanlah kekeliruan sepele.
2. Ada kesalahan yang hanya bisa ditemukan dengan bantuan proof assistant.

Ringkasan isi

• Dari Desember tahun lalu hingga 16 April tahun ini, saya menghabiskan sekitar 170 jam untuk membuktikan teorema string String.splitOn_of_valid di pustaka standar milik proof assistant Lean.
• Saat membuktikan teorema ini, saya menemukan sebuah bug dalam definisi fungsi String.splitOn.
• Memperbaiki bug ini tidak terlalu sulit. Di definisi tersebut, saya hanya perlu mengganti i menjadi i - j.
• Namun, saya tidak menganggap kesalahan ini sebagai kekeliruan sepele. Menurut definisi itu, fungsi splitOn biasanya bekerja dengan benar, tetapi dalam kasus khusus menghasilkan hasil yang salah.
• Jika saya tidak menggunakan proof assistant seperti Lean, saya tidak akan pernah bisa menemukan kesalahan yang begitu halus seperti ini.