Bukti pertama Anda

sepuluh menit · tiga langkah · tidak ada yang harus Anda percayai begitu saja

Ini adalah jalur pemula. Anda tidak perlu menjadi seorang programmer, Anda tidak perlu memiliki akun, dan Anda tidak perlu memberi tahu kami bahwa Anda ada. Pada akhirnya komputer Anda sendiri — bukan milik kami, dan bukan kata-kata kami — akan telah memeriksa matematika di balik sebuah aturan sungguhan dari pustaka.

Jika Anda sudah mengenal cara kerja sebuah pembukti, jalur lengkapnya melangkah lebih jauh: membangun front-nya dan memeriksa setiap baris tabel kebenarannya. Halaman ini berhenti tepat di buktinya, yaitu bagian yang paling penting dan bagian yang tidak memerlukan apa pun untuk dipasang.

Apa yang akan Anda periksa

Aturan ini disebut brief-fill policy. Ia memutuskan kapan seorang asisten boleh menjawab atas nama pemiliknya alih-alih bertanya kepada mereka. Empat klaim dibuat tentangnya, dan keempatnya akan segera diuji di mesin Anda:

• ia tidak pernah mengisi sebuah jawaban tanpa aturan yang mengizinkannya;
• jika penyimpanan aturan hilang, tidak ada apa pun yang lolos;
• ia tidak pernah mengarang apa pun;
• ia tidak pernah menanyakan sesuatu kepada Anda yang sudah dijawab oleh sebuah aturan.

Ini bukan janji-janji dalam sebuah tulisan blog. Ini adalah teorema-teorema, dan sebuah pembukti akan segera mencoba mematahkannya.

Langkah 1 — dapatkan pembukti

Ia gratis dan bukan milik kami — ia berasal dari komunitas Ada, bukan dari kami. Itulah maksudnya: hal yang memeriksa pekerjaan kami seharusnya bukan hal yang kami serahkan sendiri kepada Anda.

Langkah 2 — dapatkan aturannya

Anda dapat mengabaikan checksum-nya pada percobaan pertama — bukti pada langkah 3 tidak bergantung padanya. Ia ada di sana untuk saat Anda ingin memastikan bahwa berkas yang Anda terima adalah berkas yang kami publikasikan, dan itu adalah berkas yang sama yang dinamai oleh the catalogue.

Langkah 3 — minta komputer Anda memeriksanya

Buka sebuah terminal di dalam folder yang telah diekstrak dan jalankan dua baris ini:

cd brief-fill-policy/core/src
gnatprove -P proof.gpr -f -U --level=2

Tunggu. Ketika selesai, carilah dua kata ini:

0 unproved

Itu saja. Itulah keseluruhan latihannya. Tidak ada lagi yang perlu dipasang, dan langkah ini bekerja pada mesin polos yang tidak memiliki apa-apa lagi di dalamnya — pembukti yang Anda unduh membawa semua yang dibutuhkan buktinya.

Apa yang baru saja terjadi

Komputer Anda mengambil keempat klaim di atas, mencoba menemukan sebuah kasus di mana salah satunya gagal, dan tidak dapat menemukannya — karena memang tidak ada. Bukan “kami mengujinya dan tampaknya baik-baik saja”. Bukan “kata sang pemelihara”. Sebuah mesin yang tidak dapat dibujuk pergi mencari sebuah contoh tandingan dan kembali dengan tangan kosong.

Anda tidak mempercayai kami untuk memberi tahu Anda hal itu. Anda menyaksikannya terjadi pada perangkat keras milik Anda sendiri.

Opsional — rusak dia dengan sengaja

Ini adalah bagian yang layak dilakukan jika Anda punya lima menit lagi, karena sebuah pemeriksaan yang hanya selalu berkata ya tidak banyak artinya.

Buka brief_fill_policy_pkg.ads di editor teks apa pun dan ubah aturannya sehingga penyimpanan yang hilang tetap membiarkan sebuah jawaban lolos. Jalankan perintah yang sama lagi. Ia akan menolak — dan ia akan menyebutkan persis teorema yang baru saja Anda rusak.

Penolakan itu adalah keseluruhan model keamanannya. Ghillie tidak memasang apa pun yang tidak lolos ini, sehingga apa yang baru saja Anda lakukan dengan tangan sendiri adalah apa yang ia lakukan atas nama Anda setiap saat.

Apa yang tidak dibuktikan oleh ini

Kami lebih memilih mengatakan ini daripada membiarkan Anda menemukannya sendiri nanti. Bukti-bukti ini mencakup aturan-aturan keputusan — siapa yang boleh melihat apa, apa yang boleh keluar, apa yang harus dipenuhi sebuah kiriman. Bukti-bukti ini tidak membuat sisa perangkat lunaknya menjadi ajaib, dan kami tidak mengklaim bahwa mereka melakukannya. Kejujuran itulah kesepakatannya, dan itulah seluruh kesepakatannya.

Ke mana selanjutnya

• Jalur lengkapnya — membangun front-nya dan memeriksa setiap baris tabel kebenaran yang disertakan.
• The catalogue — sisa raknya, setiap bagian dapat diturunkan ulang dengan cara yang sama.
• Ghillie — asisten yang dilayani oleh aturan-aturan ini.
• The Reef machine — perangkat keras apa yang Anda butuhkan jika Anda ingin melangkah lebih jauh dari halaman ini.

Jika tidak berhasil, itu adalah sebuah temuan dan kami ingin mendengarnya. Sebuah penolakan yang tidak dapat Anda jelaskan lebih menarik bagi kami daripada sebuah keberhasilan.