Sumber: https://unsplash.com/photos/silver-and-white-round-analog-watch-beside-white-printer-paper-evixqxe715k

Pernahkah Anda bertanya, apa yang menjamin sistem navigasi pesawat atau protokol keamanan bank bekerja 100% benar? Jawabannya bukan sekadar coding yang rapi, melainkan jaminan dari metode pembuktian yang berasal dari logika matematika. Dalam dunia Computer Science, pembuktian adalah alat krusial untuk memastikan bahwa algoritma tidak hanya berfungsi, tetapi juga terbukti benar di bawah segala kondisi.

Logika Matematika: Fondasi Kepastian, Bukan Hanya Teori

Bagi sebagian orang, logika matematika hanyalah sebuah bab pada buku matematika yang berisi aturan-aturan dan rumus yang rumit. Namun, logika matematika merupakan sebuah kerangka berpikir dasar yang harus dimiliki oleh semua orang. Logika matematika sangat berkaitan erat dengan kemampuan untuk bernalar dan pengambilan keputusan yang dilakukan di kegiatan sehari-hari, dimana hal ini cukup krusial di bidang ilmu komputer.

Tanpa logika matematika, komputer yang ada pada era sekarang tidak akan tercipta. Ide awal dari komputer adalah mesin Turing yang diajukan oleh Alan Turing sekitar tahun 1936, yang muncul untuk menjawab masalah Enthscheidungsproblem; apakah sebuah pernyataan logika dapat ditentukan kebenarannya secara formal. Selain itu, semua program pada komputer dibangun oleh bahasa pemrograman seperti Fortran, C++, Python, yang pasti mengandung simbol dan struktur logika. Hal tersebut juga sangat membantu dalam merancang suatu algoritma, basis data, dan bahkan sistem kecerdasan artifisial (AI).

Salah satu topik yang cukup penting untuk dipelajari saat mempelajari logika matematika adalah metode pembuktian (methods of proof). Pembuktian sebuah pernyataan matematika (seperti teorema Pythagoras) dilakukan untuk memastikan apakah pernyataan tersebut benar dan logis. Meskipun lebih banyak digunakan untuk membuktikan keabsahan pernyataan matematis, metode pembuktian juga sangat umum digunakan dalam ilmu komputer. Dengan adanya pembuktian, para engineer dapat memberikan jaminan bahwa suatu sistem atau program sudah berjalan dengan benar sesuai ekspektasi dan spesifikasi yang ditentukan.

 

Tiga Alasan Logika Menyelamatkan Dunia Digital Kita

Pentingnya logika matematika, khususnya metode pembuktian, pada dunia digital tercermin dari tiga peran kunci:

  1. Meningkatkan Efisiensi dan Inovasi

Sumber: https://unsplash.com/photos/a-person-typing-on-a-laptop-on-a-desk-mKhPLJ5JQI4

Semua teknologi besar mulai dari cara mesin pencari Google menyortir hasil hingga chip komputer tercepat berbasis pada algoritma. Hal ini tidak akan lepas dari teori kompleksitas, yaitu teori yang mempelajari penentuan sumber daya (baik waktu maupun memori) yang dibutuhkan untuk menyelesaikan masalah komputasi dan mengklasifikasikannya berdasarkan tingkat kesulitannya. Sebuah algoritma memiliki kompleksitas waktu (waktu yang digunakan untuk menyelesaikan suatu algoritma berdasarkan ukuran input) dan kompleksitas ruang (banyak memori yang digunakan untuk menjalankan algoritma berdasarkan ukuran input) yang berbeda-beda. Metode pembuktian berguna untuk melihat apakah algoritma yang diajukan adalah paling efisien dalam hal sumber daya yang digunakan. Pembuktian efisiensi suatu algoritma juga mendorong engineer untuk menciptakan teknologi yang lebih baik daripada yang sudah terbukti sebelumnya.

 

  1. Menjamin Keandalan Sistem Kritis

Sumber: https://unsplash.com/photos/black-samsung-android-smartphone-displaying-icons-PZao9UjlbMY

 

Bidang-bidang seperti kesehatan, finansial, dan navigasi umumnya tidak mentoleransi adanya kesalahan sekecil apapun. Sistem digital seperti software yang digunakan pada bidang tersebut harus berjalan dengan benar, dan bugs yang muncul dapat memberikan dampak yang signifikan (seperti The Millenium Bug atau Y2K yang mengakibatkan kerugian sebesar 300-600 miliar USD). Hal ini dapat dihindari dengan software testing, dimana salah satu metodenya adalah formal verification: pengecekan apakah software sudah bekerja dengan benar menggunakan metode pembuktian formal seperti automated theorem proving (ATP). Software testing akan menjamin bahwa algoritma yang digunakan pada software tersebut bebas dari cacat logika, sehingga dapat diandalkan tanpa pantauan manusia secara terus-menerus.

 

  1. Membentengi Keamanan Siber

Sumber: https://unsplash.com/photos/red-padlock-on-black-computer-keyboard-mT7lXZPjk7U

 Associate Professor Toby Murray, seorang peneliti dari University of Melbourne beserta timnya mengembangkan metode bernama COVERN di tahun 2018. Metode ini bertujuan untuk membuktikan bahwa Cross Domain Desktop Compositor (CDDC), sebuah alat untuk melindungi data sensitif saat mengakses konten secara online, memanglah aman. Metode COVERN berisi aturan-aturan untuk memverifikasi keamanan CDDC yang dibangun berdasarkan logika matematika dan juga metode pembuktian. Penelitian ini menunjukkan bahwa metode pembuktian juga dapat diaplikasikan di bidang keamanan siber, dimana sebuah sistem dikatakan aman jika sistem tersebut terbukti memenuhi aturan-aturan yang ditetapkan oleh standar tertentu.

Pada akhirnya, metode pembuktian bukanlah sekadar latihan teoretis dari logika matematika, melainkan fondasi intelektual yang menopang seluruh dunia digital kita. Pembuktian adalah jaminan yang memungkinkan kita membangun teknologi yang efisien untuk inovasi, sistem yang andal untuk keselamatan publik, dan protokol yang aman untuk melindungi data kita. Di era di mana kita semakin bergantung pada software untuk aspek krusial kehidupan, kemampuan untuk tidak hanya menulis kode, tetapi juga membuktikan kebenarannya, adalah keterampilan tertinggi. Oleh karena itu, bagi setiap calon engineer dan insan Computer Science, menguasai logika dan metode pembuktian adalah langkah wajib untuk menciptakan masa depan digital yang lebih pasti dan bertanggung jawab.

 

Penulis: Rilo Chandra Pradana, S.Si., M.Kom.

Reference: