Menulis perangkat lunak yang benar dan bebas dari kesalahan merupakan tantangan yang sangat besar dalam dunia ilmu komputer. Berdasarkan teori komputabilitas dan kompleksitas, tingkat kesulitan dalam memastikan kebenaran program bukan sekadar masalah alat bantu, melainkan hukum alam dari komputasi itu sendiri.
Landasan Teoretis dan Batasan Komputasi
Sejarah teoretis ilmu komputer berakar dari upaya matematikawan David Hilbert yang ingin memformalkan seluruh matematika. Hilbert mencari prosedur keputusan untuk menentukan kebenaran setiap pernyataan formal, yang meliputi konsistensi, kelengkapan, dan keterputusan. Namun, program tersebut runtuh setelah Kurt Gödel mengumumkan teorema ketidaklengkapan, disusul oleh Alonzo Church dan Alan Turing pada tahun 1936 yang membuktikan teorema penghentian atau *halting theorem*.
Teorema penghentian menyatakan bahwa tidak mungkin ada algoritma yang dapat memutuskan apakah suatu program tertentu akan pernah berhenti atau berjalan selamanya. Teorema mendasar ini memunculkan berbagai akibat langsung yang berkaitan erat dengan verifikasi perangkat lunak, seperti masalah keterjangkauan dan Teorema Rice yang menunjukkan bahwa tidak ada algoritma untuk menentukan sifat-sifat non-trivial dari fungsi parsial.
Selain itu, terdapat pula teorema yang mengukur kompleksitas analisis program, baik dari sudut pandang dinamis maupun statis. Ukuran fungsi yang menghubungkan ukuran program dengan kesulitan membuktikan penghentiannya ternyata lebih besar daripada semua fungsi yang dapat dihitung. Bahkan, terdapat program kecil yang perilakunya tidak dapat ditentukan secara matematis karena matematika sendiri tidak cukup kuat untuk membuktikan perilakunya.
Kompleksitas Algoritma dan Verifikasi
Masalah verifikasi tidak hanya soal dapat diputuskan atau tidak, tetapi juga menyangkut waktu dan upaya yang dibutuhkan. Mengutip dari Hacker News: Front Page (pron.github.io), teori kompleksitas komputasi yang dipelopori oleh Juris Hartmanis dan Richard Stearns menunjukkan bahwa masalah komputasi membentuk hierarki kesulitan yang tak terbatas. Pertanyaan mengenai kompleksitas memutuskan apakah suatu program berhenti dalam langkah tertentu menunjukkan bahwa Anda tidak dapat mengetahui apa yang akan dilakukan oleh sebuah program lebih cepat daripada menjalankannya.
Verifikasi didefinisikan sebagai masalah yang paling sulit dalam ilmu komputer. Ketika dicoba diurai dengan membatasi bahasa pemrograman menjadi bahasa total—di mana semua perulangan memiliki penghitung yang dikurangi—verifikasi tetap berada pada tingkat kesulitan yang sama. Bahkan program sederhana yang ditulis dengan gaya total terkadang menyembunyikan masalah teori bilangan yang belum terpecahkan selama ratusan tahun, seperti konjektur Goldbach.
Upaya untuk mempermudah verifikasi melalui modularisasi program juga menemui jalan buntu karena kebenaran perangkat lunak tidak dapat diuraikan secara terpisah (*correctness does not decompose*). Kompleksitas verifikasi dari komponen-komponen yang digabungkan tetap tidak dapat ditangani dengan mudah, membuktikan bahwa bahasa pemrograman dengan abstraksi canggih pun tidak secara otomatis membuat verifikasi menjadi layak secara praktis.
Meskipun verifikasi penuh tidak mungkin dilakukan untuk setiap program sepanjang waktu, batasan teoretis ini tidak menghentikan upaya untuk memverifikasi beberapa program pada waktu tertentu untuk properti-properti tertentu.
Sumber: Hacker News: Front Page
