Apa yang kita ketahui tentang program yang terbukti benar?

Semakin kompleksnya program komputer dan semakin pentingnya posisi komputer dalam masyarakat kita membuat saya bertanya-tanya mengapa kita masih belum secara kolektif menggunakan bahasa pemrograman di mana Anda harus memberikan bukti formal bahwa kode Anda berfungsi dengan benar.

Saya percaya istilah ini adalah 'kompiler sertifikasi' (saya menemukannya di sini ): kompiler mengkompilasi bahasa pemrograman di mana seseorang tidak hanya harus menulis kode, tetapi juga menyatakan spesifikasi kode dan membuktikan bahwa kode mematuhi spesifikasi (atau gunakan pepatah otomatis untuk melakukannya).

Saat mencari di internet, saya hanya menemukan proyek yang menggunakan bahasa pemrograman yang sangat sederhana atau proyek gagal yang mencoba menyesuaikan bahasa pemrograman modern. Ini mengarahkan saya ke pertanyaan saya:

Apakah ada kompiler sertifikasi yang menerapkan bahasa pemrograman full-blown, atau apakah ini sangat sulit / secara teori tidak mungkin?

Selain itu, saya belum melihat adanya kelas kerumitan yang melibatkan program yang dapat dibuktikan, seperti 'kelas semua bahasa yang dapat diputuskan oleh mesin Turing yang ada buktinya bahwa mesin Turing ini berhenti', yang saya sebut $ProvableR$ , sebagai analog dengan $R$ , himpunan bahasa rekursif.

Saya dapat melihat keuntungan dari mempelajari kelas kompleksitas seperti itu: misalnya, untuk $ProvableR$ masalah Putus dapat ditentukan (saya bahkan menduga $ProvableRE$ didefinisikan dengan cara yang jelas adalah kelas bahasa terbesar yang dapat dipilih). Selain itu, saya ragu kami akan mengesampingkan program praktis yang berguna: siapa yang akan menggunakan program ketika Anda tidak dapat membuktikannya berakhir?

Jadi pertanyaan kedua saya adalah:

Apa yang kita ketahui tentang kelas kompleksitas yang membutuhkan bahasa mereka yang mengandung memiliki properti tertentu?

"Penyusun penyertifikasi" biasanya berarti sesuatu yang sedikit berbeda: itu berarti Anda memiliki penyusun yang dapat membuktikan bahwa kode mesin yang dipancarkannya dengan benar mengimplementasikan semantik tingkat tinggi. Artinya, ini adalah bukti bahwa tidak ada bug kompiler. Program yang diberikan orang ke kompiler masih bisa salah, tetapi kompiler akan menghasilkan versi kode mesin yang benar dari program yang salah. Kisah sukses terbesar di sepanjang baris ini adalah kompiler terverifikasi CompCert , yang merupakan kompiler untuk sebagian besar dari C.

Compiler Compcert itu sendiri adalah sebuah program dengan bukti kebenaran (dilakukan dalam Coq), yang menjamin bahwa jika menghasilkan kode untuk suatu program, itu akan benar (sehubungan dengan semantik operasional perakitan & C yang digunakan desainer CompCert). Upaya memeriksa mesin-mesin ini cukup besar; biasanya bukti kebenarannya berkisar antara 1x hingga 100x ukuran program yang Anda verifikasi. Menulis program dan bukti yang diperiksa dengan mesin adalah keterampilan baru yang harus Anda pelajari - ini bukan matematika atau pemrograman seperti biasa, meskipun itu tergantung pada kemampuan untuk melakukan keduanya dengan baik. Rasanya seperti Anda mulai dari awal, seperti menjadi programmer pemula lagi.

Tidak ada hambatan teoretis khusus untuk ini. Satu-satunya hal di sepanjang baris ini adalah teorema Blum Size bahwa untuk semua bahasa di mana semua program total, Anda dapat menemukan program dalam bahasa rekursif umum yang akan setidaknya secara eksponensial lebih besar ketika diprogram dalam bahasa total. Cara untuk memahami hasil ini adalah bahwa bahasa total mengkodekan tidak hanya sebuah program, tetapi juga bukti terminasi. Jadi, Anda dapat memiliki program pendek dengan bukti terminasi panjang. Namun, ini tidak terlalu penting dalam praktik, karena kita hanya akan pernah menulis program dengan bukti terminasi yang dapat dikelola.

EDIT: Dai Le meminta penjelasan tentang poin terakhir.

Ini sebagian besar merupakan klaim pragmatis, berdasarkan pada fakta bahwa jika Anda dapat memahami mengapa suatu program bekerja, maka tidak mungkin bahwa alasannya adalah berjuta-juta halaman sepanjang invarian. (Invarian terpanjang yang pernah saya gunakan adalah beberapa halaman, dan apakah mereka membuat pengulas menggerutu! Dapat dimengerti juga, karena invarian adalah alasan mengapa program bekerja menghilangkan semua narasi yang membantu orang memahaminya.)

Tetapi ada juga beberapa alasan teoretis juga. Pada dasarnya, kita tidak tahu banyak cara untuk secara sistematis menciptakan program yang bukti kebenarannya sangat panjang. Metode utama adalah (1) mengambil logika di mana Anda membuktikan kebenaran, (2) menemukan properti yang tidak dapat secara langsung dinyatakan dalam logika itu (bukti konsistensi adalah sumber khas), dan (3) menemukan program yang bukti kebenaran bergantung pada keluarga konsekuensi yang dapat diungkapkan dari properti yang tidak dapat diungkapkan. Karena (2) tidak dapat diekspresikan, ini berarti bahwa bukti dari setiap konsekuensi yang dapat diekspresikan harus dilakukan secara independen, yang memungkinkan Anda meledakkan ukuran bukti kebenaran. Sebagai contoh sederhana, perhatikan bahwa dalam logika tingkat pertama dengan relasi induk, Anda tidak bisa mengekspresikan relasi leluhur.$k$$k$) dapat diekspresikan, untuk setiap tetap . Jadi dengan memberikan program yang menggunakan beberapa properti leluhur hingga beberapa kedalaman (katakanlah, 100), Anda dapat memaksa bukti kebenaran dalam FOL untuk memuat bukti dari properti tersebut seratus kali lipat.$k$

Pandangan canggih tentang subjek ini disebut "matematika terbalik", dan merupakan studi yang mengharuskan aksioma untuk membuktikan teorema yang diberikan. Saya tidak tahu banyak tentang itu, tetapi jika Anda memposting pertanyaan tentang aplikasinya ke CS, dan saya yakin setidaknya Timothy Chow, dan mungkin beberapa orang lain, akan dapat memberi tahu Anda hal-hal menarik.

Saya pikir jawaban untuk pertanyaan pertama adalah bahwa umumnya terlalu banyak bekerja dengan alat saat ini. Untuk mendapatkan perasaan, saya sarankan mencoba untuk membuktikan kebenaran Bubble Sort dalam Coq (atau jika Anda lebih suka sedikit tantangan, gunakan Quick Sort). Saya tidak berpikir masuk akal untuk mengharapkan programmer menulis program yang diverifikasi asalkan membuktikan kebenaran dari algoritma dasar seperti itu sangat sulit dan memakan waktu.

Pertanyaan ini mirip dengan menanyakan mengapa ahli matematika tidak menulis bukti formal yang dapat diverifikasi oleh pemeriksa bukti? Menulis program dengan bukti kebenaran formal berarti membuktikan teorema matematika tentang kode tertulis, dan jawaban untuk pertanyaan itu juga berlaku untuk pertanyaan Anda.

Ini tidak berarti bahwa belum ada kasus yang berhasil dari program yang diverifikasi. Saya tahu bahwa ada kelompok yang membuktikan kebenaran sistem seperti hypervisor Microsoft . Kasus terkait adalah Microsoft C Compiler Terverifikasi . Tetapi secara umum alat saat ini membutuhkan banyak pengembangan (termasuk aspek SE dan HCI mereka) sebelum menjadi berguna bagi programmer umum (dan ahli matematika).

Mengenai paragraf terakhir dari jawaban Neel tentang pertumbuhan ukuran program untuk bahasa dengan hanya fungsi total, sebenarnya mudah untuk membuktikan lebih banyak lagi (Jika saya memahaminya dengan benar). Adalah masuk akal untuk mengharapkan bahwa sintaks dari bahasa pemrograman apa pun akan ce dan himpunan fungsi komputasi total tidak ce, jadi untuk bahasa pemrograman mana pun semua program total ada fungsi komputasi total yang tidak dapat dihitung oleh program apa pun ( dalam ukuran berapa pun) dalam bahasa itu.

Untuk pertanyaan kedua, saya menjawab pertanyaan serupa di blog Scott beberapa waktu yang lalu. Pada dasarnya jika kelas kompleksitas memiliki karakterisasi yang bagus dan dapat dihitung secara representatif (yaitu ce) maka kita dapat membuktikan bahwa beberapa representasi masalah dalam kelas kompleksitas terbukti total dalam teori yang sangat lemah sesuai dengan kelas kompleksitas. Ide dasarnya adalah bahwa provably keseluruhan fungsi dari teori berisi semua fungsi dan masalah yang A C $AC^0$$AC^0$-lengkap untuk kelas kompleksitas, oleh karena itu berisi semua masalah di kelas kompleksitas dan dapat membuktikan totalitas program-program tersebut. Hubungan antara bukti dan teori kompleksitas dipelajari dalam kompleksitas bukti, lihat buku terbaru SA Cook dan P. Nguyen " Yayasan Logistik Kompleksitas Bukti " jika Anda tertarik. ( Draf dari 2008 tersedia.) Jadi jawaban dasarnya adalah bahwa untuk banyak kelas "Terbukti C = C".

Ini tidak benar secara umum karena ada kelas kompleksitas semantik yang tidak memiliki karakterisasi sintaksis, misalnya total fungsi yang dapat dihitung. Jika dengan rekursif yang Anda maksud adalah fungsi rekursif total maka keduanya tidak sama, dan himpunan fungsi yang dapat dihitung yang terbukti total dalam suatu teori dipelajari dengan baik dalam literatur teori pembuktian dan disebut fungsi total yang dapat dibuktikan dari teori. Sebagai contoh: provably Total fungsi adalah ε 0 fungsi -recursive (atau ekuivalen fungsi dalam sistem Godel T ), yang provably keseluruhan fungsi dari P A 2 adalah fungsi dalam Girard sistem F , yang provably Total fungsi$PA$$\epsilon_0$$T$$PA^2$$F$ adalah fungsi rekursif primitif, ....$I\Sigma_1$

Tetapi bagi saya tampaknya hal ini tidak banyak berarti dalam konteks verifikasi program, karena ada juga program yang secara komputasi menghitung fungsi yang sama tetapi kami tidak dapat membuktikan bahwa kedua program tersebut menghitung fungsi yang sama, yaitu program-program tersebut secara ekstensi sama tetapi tidak sengaja. (Ini mirip dengan Bintang Fajar dan Bintang Sore.) Selain itu, mudah untuk memodifikasi program total terbukti yang diberikan untuk mendapatkan satu yang teorinya tidak dapat membuktikan totalitasnya.

$P$$n$$n$$P$algoritma untuk faktorisasi dari buktinya. (Ada juga peneliti yang mencoba mengotomatiskan pendekatan pertama sebanyak mungkin, tetapi memeriksa properti non-sepele yang menarik dari program sulit secara komputasi dan tidak dapat sepenuhnya diverifikasi tanpa positif dan negatif palsu.)

Apa yang Anda tanyakan dalam pertanyaan pertama kadang-kadang disebut "kompiler verifikasi", dan beberapa tahun yang lalu Tony Hoare menawarkannya sebagai tantangan besar untuk riset komputasi . Hingga taraf tertentu ini sudah ada dan sedang aktif digunakan dalam alat-alat seperti Coor theorem prover , yang mengatur masalah dengan cara teori jenis dan prinsip proposisi-sebagai-tipe (" Curry-Howard ").

EDIT: hanya ingin menambahkan penekanan pada "sampai batas tertentu". Ini jauh dari masalah yang diselesaikan, tetapi keberhasilan Coq memberi harapan bahwa itu bukan mimpi pipa.

Alat yang memeriksa apakah suatu program benar kadang-kadang disebut verifikasi program. Dalam konteks ini, "benar" biasanya berarti dua hal: bahwa program tidak pernah menghasilkan output tertentu (pikirkan kesalahan segmentasi, NullPointerException, dll.) Dan bahwa program setuju dengan spesifikasi.

Kode dan spesifikasinya mungkin setuju dan masih dianggap salah. Dalam arti tertentu, meminta pengembang untuk menulis spesifikasi seperti meminta dua pengembang untuk menyelesaikan masalah. Jika kedua implementasi setuju maka Anda memiliki keyakinan yang lebih tinggi bahwa mereka baik-baik saja. Namun, dalam arti lain, spesifikasi lebih baik daripada implementasi kedua. Karena spesifikasi tidak perlu efisien atau bahkan dapat dieksekusi, itu bisa jauh lebih ringkas dan karenanya lebih sulit untuk salah.

Dengan peringatan ini dalam pikiran, saya sarankan Anda melihat verifikasi program Spec # .

Dalam kasus umum, tidak mungkin untuk membuat algoritma yang mengkonfirmasi apakah suatu algoritma setara dengan spesifikasi. Ini adalah bukti informal:

Hampir semua bahasa pemrograman Turing-lengkap. Oleh karena itu, bahasa apa pun yang diputuskan oleh TM juga dapat diputuskan oleh program yang ditulis dalam bahasa ini.

$Equivalence/TM$

$Equivalence/TM$$Non-emptiness/TM$$Emptiness/TM$$Emptiness/TM$$Equivalence/TM$$Equivalence/TM$juga tidak bisa diterima. Karena itu Anda dapat menggunakan suatu algoritma apakah dua mesin tidak setara atau tidak, tetapi Anda tidak dapat memastikan apakah mereka setara, atau Anda belum memberikan algoritma Anda cukup waktu.

Namun, ini hanya untuk kasus umum. Ada kemungkinan bahwa Anda dapat memutuskan apakah spesifikasinya setara dengan program, dengan memecahkan versi masalah yang lebih santai. Misalnya, Anda dapat memeriksa hanya sejumlah input atau mengatakan bahwa kedua program tersebut setara dengan beberapa ketidakpastian. Inilah yang dimaksud dengan pengujian perangkat lunak.

Adapun sisa pertanyaan Anda:

Catatan: Bagian ini telah diedit untuk klarifikasi. Ternyata saya melakukan kesalahan yang saya coba hindari, maaf.

$TrueR$$TrueR \subseteq R$

$ProvableR = TrueR$$ProvableR \subset TrueR$$TrueR \subset ProvableR$$A \epsilon TrueR$$A$$A$$A \epsilon ProvableR$

Secara informal, ini dapat diringkas sebagai: Anda tidak tahu bahwa suatu bahasa dapat ditentukan sampai Anda membuktikannya. Jadi jika dalam sistem formal Anda memiliki pengetahuan bahwa suatu bahasa dapat dipilih, pengetahuan ini juga dapat berfungsi sebagai bukti untuk itu. Oleh karena itu, Anda tidak dapat secara bersamaan memiliki pengetahuan bahwa suatu bahasa dapat dipilih dan tidak dapat dibuktikan demikian, kedua pernyataan ini saling eksklusif.

$R$$ProvableR$$ProvableR \subset R$$R$

@Kaveh merangkumnya dengan sangat baik: Dapat dibuktikan selalu berarti dapat dibuktikan dalam beberapa sistem / teori dan tidak sesuai dengan kebenaran secara umum.

Hal yang sama berlaku untuk kelas kompleksitas lainnya: Untuk menentukan keanggotaan Anda perlu bukti terlebih dahulu. Inilah mengapa saya percaya bahwa pertanyaan kedua Anda terlalu umum, karena tidak hanya berisi teori kompleksitas, tetapi juga teori komputasi, tergantung pada properti yang Anda inginkan bahasa.

Studi monograf klasik berikut hampir persis dengan pertanyaan kedua Anda:

Hartmanis, J. Perhitungan yang layak dan sifat kompleksitas yang dapat dibuktikan , Seri Konferensi Regional CBMS-NSF dalam Matematika Terapan, 30. Masyarakat untuk Industri dan Matematika Terapan (SIAM), Philadelphia, Pa., 1978.

$\{L(M_i) | T_i(n) \leq T(n) \text{ is provable in F}\}$$M_i$$T_i(n)$$M_i$$n$

$T(n) \geq n \log(n)$$g(n) \geq 1$$F$$TIME[T(n)] \subsetneq TIME[T(n) g(n)]$

$T(n)$$F$$TIME[T(n)] \neq TIME[T(n)]$

$T(n) \geq n \log(n)$$TIME[T(n)] = \{ L(M_i) | \text{F proves} (\exists j)[L(M_j) = L(M_i) \wedge T_j(n) \leq T(n)] \}$

Namun untuk ruang, situasinya lebih terkontrol:

$s(n) \geq n$$SPACE[s(n)] = F$$SPACE[s(n)]$

$SPACE[S(n)]=F$$SPACE[S(n)]$$S(n) \geq n$$s(n)$$SPACE[S(n)]=SPACE[s(n)]$

Pertanyaan harus diajukan dengan benar. Sebagai contoh, tidak ada yang pernah ingin tahu apakah suatu program aktual akan selesai diberikan memori tak terbatas dan beberapa cara mengaksesnya (mungkin operasi untuk memindahkan alamat pangkalan dengan beberapa nomor). Teorema Turing tidak relevan dengan kebenaran program dalam arti konkret dan orang-orang yang menyebutnya sebagai penghambat verifikasi program membingungkan dua hal yang sangat berbeda. Ketika insinyur / programmer berbicara tentang kebenaran program, mereka ingin tahu tentang properti yang terbatas. Ini juga cukup benar untuk matematikawan yang tertarik pada apakah sesuatu dapat dibuktikan. Surat Godel http://vyodaiken.com/2009/08/28/godels-lost-letter/ menjelaskan hal ini secara terperinci.

Yaitu, itu jelas akan berarti bahwa meskipun keraguan Entscheidungsproblem, pekerjaan mental seorang ahli matematika tentang pertanyaan Ya atau Tidak dapat sepenuhnya diganti oleh mesin. Lagi pula, orang hanya harus memilih bilangan alami dan begitu besar sehingga ketika mesin tidak memberikan hasil, tidak masuk akal untuk berpikir lebih banyak tentang masalahnya.

Mungkin tidak layak untuk memeriksa serangkaian besar program yang dijalankan pada komputer yang sebenarnya dan mendeteksi keadaan yang buruk, tidak ada alasan teoretis mengapa hal itu tidak dapat dilakukan. Faktanya, ada banyak kemajuan di bidang ini - misalnya lihat http://www.cs.cornell.edu/gomes/papers/SATSolvers-KR-book-draft-07.pdf (terima kasih kepada Neil Immerman untuk bercerita tentang ini)

Masalah yang berbeda dan lebih sulit adalah menentukan dengan tepat properti apa yang ingin dimiliki suatu program agar benar.