Metode Formal: Hanya Praktik Rekayasa yang Baik? (2024)

 (brooker.co.za)
1 poin oleh GN⁺ 2025-01-12 | 1 komentar | Bagikan ke WhatsApp
  • Dalam sistem berskala besar, terdistribusi, dan sistem low-level yang penting, metode formal harus dilihat bukan sebagai prosedur tambahan semata untuk correctness, melainkan sebagai praktik rekayasa yang menghemat waktu dan biaya
  • Dalam perangkat lunak, desain dan implementasi mudah bercampur, sehingga perubahan desain yang terlambat langsung berujung pada pengerjaan ulang implementasi dan biaya perubahan API
  • Meninjau perilaku dan antarmuka secara konkret sebelum implementasi dapat mengurangi kepadatan bug dan masalah setelah produksi, serta membantu mencapai desain yang benar dengan lebih cepat
  • Di area yang sulit diformalisasi, seperti kebutuhan pengguna yang cepat berubah atau UI, dokumentasi, dan logika harga, manfaat desain formal menyeluruh di awal bisa menurun
  • Alat seperti TLA+ dan P juga dapat digunakan untuk meninjau optimisasi dan constraint pada tahap desain, sehingga mengurangi trade-off antara correctness dan performa

Metode Formal sebagai Praktik Rekayasa yang Baik

  • Metode formal adalah bagian penting dari praktik software engineering yang baik
  • Nilai penerapannya sangat besar terutama bagi engineer yang menangani sistem berskala besar, sistem terdistribusi, dan sistem low-level yang penting
  • Berangkat dari premis bahwa rekayasa pada akhirnya adalah aktivitas untuk mengoptimalkan waktu dan biaya
    • Performa, skalabilitas, keberlanjutan, dan efisiensi juga ikut dipertimbangkan
  • Metode formal tidak murah atau mudah, dan tidak selalu cocok untuk semua cara pengembangan, tetapi intuisi bahwa metode ini hanya menambah biaya tidak selalu benar

Dua Jalur untuk Mengurangi Biaya

  • Yang pertama adalah mengurangi pengerjaan ulang
    • Tidak seperti bidang rekayasa lain, dalam perangkat lunak desain dan pembangunan cenderung terjadi secara bersamaan
    • Implementasi bisa dimulai meskipun desain belum cukup matang
    • Fleksibilitas seperti ini adalah kekuatan perangkat lunak, tetapi dapat mengubah iterasi desain menjadi iterasi implementasi sehingga biaya membesar
  • Yang kedua adalah mengelola biaya perubahan
    • Begitu sebuah API atau sistem memiliki pelanggan, perubahan menjadi jauh lebih mahal dan sulit
    • Menurut Hyrum’s Law, ketika jumlah pengguna API cukup banyak, terlepas dari isi kontraknya, akan ada seseorang yang bergantung pada setiap perilaku yang dapat diamati
  • Mengisolasi perilaku sistem melalui API adalah gagasan penting dalam software engineering, tetapi tetap ada batasan bahwa pengguna dapat bergantung bahkan pada detail implementasi
  • Sistem di balik API mungkin bisa diimplementasikan ulang sepenuhnya, tetapi abstraksi tidak menghilangkan biaya perubahan itu sendiri
  • Pekerjaan desain formal dapat mengurangi biaya pengerjaan ulang dan memindahkan perubahan antarmuka ke waktu yang lebih awal, sehingga meningkatkan kecepatan dan efisiensi pembangunan perangkat lunak

Sistem yang Cocok untuk Desain Formal

  • Tidak diterapkan dengan cara yang sama pada semua perangkat lunak
  • Pada perangkat lunak yang cepat berevolusi atau memiliki banyak kebutuhan pengguna yang sulit diformalisasi, nilai desain di awal bisa melemah
    • UI, situs web, dan implementasi logika harga termasuk dalam kategori ini
    • Di area seperti ini, banyak pengerjaan ulang yang berkelanjutan dapat membuat biaya desain di awal menjadi besar
  • Gagasan dasar agile adalah menjalankan implementasi dan pengumpulan kebutuhan secara paralel untuk mengurangi waktu menuju rilis
    • Memungkinkan implementasi tetap diselesaikan meskipun pengumpulan kebutuhan terus berlangsung
    • Dalam banyak kasus, cara pengembangan paralel seperti ini optimal atau menjadi prasyarat penting agar pekerjaan dapat berjalan
  • Sebaliknya, banyak bagian dari sistem berskala besar, terdistribusi, dan low-level memiliki kebutuhan yang sudah dipahami dengan baik
    • Setidaknya ada bagian kebutuhan statis yang cukup besar
    • Dalam kasus ini, desain formal di awal dapat secara signifikan mengurangi pengerjaan ulang dan kepadatan bug pada tahap implementasi maupun setelah produksi
  • Semakin dekat kebutuhan pada hukum fisika, semakin besar nilai desain dan desain formal; semakin dekat pada opini pengguna, semakin kecil nilainya

Dokumentasi Kebutuhan dan Batas Formalisasi

  • Menuliskan kebutuhan pengguna secara jelas sangat bernilai, baik formal maupun informal
  • Jika kebutuhan tidak ditulis, waktu akan terbuang dan gesekan dapat muncul karena orang bergerak ke arah yang berbeda-beda
  • Menspesifikasikan semua kebutuhan manusia secara formal bisa sulit atau tidak ekonomis
    • Kebutuhan estetika UI
    • Keterbacaan dokumentasi
    • Konsistensi nama API
  • Perbedaan pendapat tentang pendekatan formal juga muncul dari perbedaan pemikiran tentang apa itu pendekatan formal dan dengan cara apa pendekatan tersebut bernilai
  • Pendekatan seperti UML yang memindahkan kode ke diagram yang sangat banyak dapat bernilai rendah jika tidak mampu menangani pertanyaan sulit secara langsung
    • Jika dilakukan dengan cara atau alat yang buruk, pekerjaan yang bernilai pun bisa menjadi tidak berguna

Metode dan Alat Formal yang Berguna di Lapangan

  • Metode formal dan penalaran otomatis adalah bidang yang luas, dengan berbagai alat
  • Kumpulan alat yang berguna di area sistem cloud besar adalah sebagai berikut
    • Bahasa spesifikasi seperti P, TLA+, dan Alloy, beserta model checker terkait
    • Alat simulasi deterministik seperti turmoil
      • Digunakan bersama fuzzing untuk menjelajahi state space secara sistematis melalui pengujian
    • Bahasa pemrograman yang ramah verifikasi seperti Dafny dan verifier kode seperti Kani
    • Teknik simulasi numerik
    • Metode yang mendekati formal, seperti menggambar decision table, truth table, dan state machine eksplisit di whiteboard atau dokumen desain
  • Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3 adalah titik awal untuk mempelajari metode formal ringan
  • Verifikasi implementasi bukan satu-satunya tujuan
    • Alat seperti TLA+ dan P punya nilai besar untuk meninjau desain dengan lebih cepat dan konkret sebelum implementasi

Membuat Perangkat Lunak yang Lebih Cepat dengan Lebih Cepat

  • Saat How Amazon Web Services Uses Formal Methods ditulis pada 2015, fokusnya terutama pada correctness
    • Memverifikasi properti safety dan liveness dari desain
    • Mencapai desain yang benar dengan lebih cepat
  • Dalam kasus tim yang menggunakan TLA+ untuk sistem manajemen lock internal, poin pentingnya adalah mereka “memverifikasi optimisasi agresif”
  • Alat seperti TLA+ tidak hanya dapat membuat pembangunan sistem menjadi lebih cepat, tetapi juga dapat membantu membuat sistem yang lebih cepat
    • Menjelajahi optimisasi yang mungkin dengan cepat
    • Menemukan constraint yang benar-benar penting
    • Memastikan apakah optimisasi yang diusulkan benar
  • Dalam banyak kasus, metode formal mengurangi trade-off sulit antara correctness dan performa yang mudah menjebak sistem

Nilai Alat yang Dipakai pada Tahap Desain

  • Menggunakan alat yang membantu memikirkan desain sistem pada tahap desain dapat sangat meningkatkan kecepatan pengembangan perangkat lunak
  • Mengurangi risiko dan memungkinkan pembuatan sistem yang lebih teroptimasi sejak awal
  • Bagi engineer yang membangun sistem berskala besar dan kompleks, metode formal adalah bagian dari praktik rekayasa yang baik

Bacaan terkait

1 komentar

 
GN⁺ 2025-01-12
Komentar Hacker News

  • Verifikasi formal perangkat lunak, seperti diakui dalam tulisan tersebut, sangat bergantung pada jenis perangkat lunak dan proses pengembangannya
    Untuk memakai verifikasi formal, harus ada kebutuhan formal atas perilaku perangkat lunak, tetapi sebagian besar proyek dan filosofi desain tidak cocok dengan ini. Jika pengembangan dan desain berjalan bersamaan ketika apa yang diinginkan pun belum jelas, teknik formal sulit diterapkan. Namun bidang yang bergantung pada spesifikasi awal, seperti sistem kecil yang kritis bagi keselamatan, bisa memperoleh manfaat besar; perangkat lunak kedirgantaraan adalah contoh utamanya

    • Saya tidak merasa itu seniche itu. Biaya yang dibicarakan orang sudah banyak turun selama beberapa dekade terakhir, dan saya pernah mengajarkan alat seperti TLA+ atau Alloy kepada developer dalam waktu kurang dari seminggu
      Saat ini ini bukan lagi keterampilan yang membutuhkan gelar PhD atau riset bertahun-tahun untuk dipelajari, begitu pula menulis spesifikasi tingkat tinggi dasar. Dengan memakai model checker, Anda akan mempelajari sesuatu tentang sistem yang Anda modelkan, dan itu berguna meski hanya dipakai untuk dokumentasi atau pelatihan. Kekuatan mendasar teknik formal adalah memaksa kita berpikir sampai tuntas. Banyak developer percaya mereka bisa mengimplementasikan algoritma konkurensi hanya dengan kepala sendiri, type checker, dan sedikit unit test, tetapi setelah menjalankan model checker lalu menemukan kesalahan dalam desain dan asumsi, mereka pasti menjadi rendah hati. Ada banyak sistem terdistribusi yang lebih kecil dari perkiraan, dan state space sering kali jauh lebih besar daripada dugaan sebelum diformalkan
    • Ini bukan soal semua atau tidak sama sekali. Saya menangani backend yang sangat berorientasi produk dan tidak sepenuhnya dispesifikasikan, tetapi sebagian darinya saya spesifikasikan secara formal
      Misalnya, saya memasang pengujian berbasis properti pada sebuah state machine yang sangat rumit untuk memastikan bahwa, input aneh apa pun yang dipakai saat memanggil endpoint, state machine internal tidak melakukan transisi yang tidak valid. Kode di sekitarnya tidak punya spesifikasi formal, tetapi state machine tersebut punya, sehingga ini mungkin dilakukan, dan kami juga menemukan bug halus yang tidak akan pernah tertangkap oleh unit test tradisional
    • “Formal” berarti “ditulis dalam bahasa yang dapat diinterpretasikan komputer”, dan itulah yang dilakukan programmer. Menulis kode berarti menulis spesifikasi formal atas perilaku program, dan menurut definisi semua perangkat lunak harus melakukannya
      Namun untuk memperoleh manfaat teknik formal, perilaku program harus dibandingkan dengan sesuatu selain program itu sendiri, dan sesuatu yang lain itu juga harus ditulis dalam bahasa formal. Kita harus memahami secara tepat perilaku yang diinginkan, tetapi tidak perlu mencakup seluruh perilaku perangkat lunak. Unit test otomatis juga merupakan spesifikasi formal, dan menjalankannya adalah metode verifikasi formal. Itu hanya spesifikasi dan verifikasi yang lebih lemah daripada teknik formal yang biasanya dibicarakan; secara konseptual maupun praktis tidak ada perbedaan kualitatif yang jelas. Jika suatu perangkat lunak dapat diuji, besar kemungkinan metode spesifikasi formal yang lebih kaya juga bisa diterapkan, dan efektivitas biayanya dipelajari lewat coba-coba seperti saat belajar pengujian
    • Mau tidak mau, kebutuhan akan muncul. Bedanya hanya apakah kebutuhan itu ditemukan pada tahap rekayasa kebutuhan, diverifikasi dengan dokumen teks sederhana dan konfliknya dibereskan; diketahui setelah salah dibuat sambil coding; atau ditemukan pelanggan dalam “sprint review”
      Pada akhirnya ini soal seberapa banyak uang dan waktu tambahan yang ingin dibelanjakan agar bisa disebut “agile”. Secara paradoks, tahap kebutuhan tradisional adalah yang termurah di antara tiga cara itu, dan paling sesuai dengan semangat agile yang asli karena cepat mencapai konvergensi dengan pelanggan pada saat biaya perubahan paling murah: mengubah satu baris teks
    • Intinya tampaknya lebih dekat ke kemungkinan formalisasi daripada desain di muka. Misalnya, sistem otomatisasi klaim asuransi sering kali tidak bisa dirancang dari awal karena perilaku perusahaan asuransi tidak terdokumentasi, tetapi sistem otomatisasi itu dapat disempurnakan sambil memperoleh informasi lewat interaksi
      Meski begitu, kita tetap bisa mendapatkan manfaat berupa memastikan apakah semua kasus sudah tercakup dan apakah tidak ada kontradiksi di dalam sistem

  • Saya sering melihat argumen tentang metode formal seperti “perangkat lunak itu besar, kompleks, dan sulit dibuat benar; karena itu, metode formal”
    Di satu sisi, saya berharap itu benar. Saya kuat dalam cara belajar akademis, jadi secara pribadi itu menguntungkan, dan secara praktis juga menjengkelkan ketika perangkat lunak benar-benar kompleks lalu kita harus mencari-cari penyebab kegagalan. Namun jarang ada yang menunjukkan secara meyakinkan bagaimana metode formal menyelesaikan masalah itu. Tulisan ini lebih baik karena menunjukkan bahwa sebagian besar “desain” modern adalah buang-buang waktu, tetapi tidak cukup menjelaskan mengapa TLA lebih baik daripada UML. Kedengarannya seperti menyiratkan bahwa jika Anda menginvestasikan beberapa bulan atau tahun pada TLA, Anda akan mendapat pencerahan, dan memahami kegunaannya dengan cara yang tak bisa dijelaskan kepada orang yang belum tercerahkan. Kalkulus atau statistik Bayes juga punya sisi seperti itu, jadi bukan hal yang mustahil, tetapi akhirnya kita kembali pada penilaian ala manajer proyek: “kalau memang sebegitu bergunanya, lebih banyak orang pasti sudah memakainya dan manfaatnya akan terlihat dengan sendirinya.” Kalau sesuatu sudah ada sejak lama tetapi belum diadopsi luas, besar kemungkinan ada alasannya

    • Menurut saya UML tidak berguna karena diagram yang sama bisa dipahami berbeda oleh tiap orang, dan meskipun sangat kompleks, ia tidak dapat diperiksa, sehingga kita bisa membuat diagram UML yang kontradiktif atau tidak masuk akal
      Ketika menghadapi masalah yang sulit dipikirkan, kita akan memakai suatu “metode”. Untuk protokol komunikasi, bagus jika dijelaskan dengan mesin status, dan TLA lebih cocok untuk ceruk itu. Belakangan ini tidak banyak masalah yang membenarkan upaya sebesar itu, tetapi jika masalah seperti itu muncul, nilainya luar biasa. Bahasa khusus domain juga serupa: untuk menghindari berbagai masalah, jauh lebih baik memakai framework parser daripada menulis parser sendiri. Saat ini sebagian besar pengerjaan ulang berasal dari perubahan kebutuhan dan dari pelanggan yang berkata “bukan begitu” tanpa tahu apa yang sebenarnya mereka inginkan. Memang orang yang mengajukan permintaan sering tidak memikirkan implikasi kebutuhannya dengan cukup, tetapi masalah yang lebih besar adalah pengetahuan untuk mengambil keputusan yang baik tidak cukup terkumpul di satu tempat
    • Menurut saya alasan metode formal tidak banyak dipakai adalah karena tidak banyak bidang bisnis yang perlu menghabiskan banyak waktu dan biaya untuk menaikkan akurasi logika domain dari 98% menjadi 99,99%
      Metode formal jelas merupakan investasi besar. Namun meski secara umum tidak mapan, sebagian idenya telah masuk ke sistem tipe modern
    • Saya hanya pernah bersentuhan dengan verifikasi formal dalam konteks kelas perangkat keras; mirip dengan pemrograman, tetapi efektivitas dibanding biayanya benar-benar berbeda. Chip fisik tidak mudah diperbaiki setelah dibuat, dan jenis desainnya juga sangat berbeda
      Kesan yang saya dapat adalah bahwa ketatnya verifier formal membatasi kompleksitas desain, sekadar karena ia harus selesai dalam waktu dan memori yang masuk akal. Mungkin kemenangan sesungguhnya dari mewajibkan verifikasi formal adalah memperbaiki masalah “perangkat lunak itu besar, kompleks, dan sulit dibuat benar” dengan membuat program besar dan kompleks menjadi merepotkan untuk ditangani
    • Untuk merebus katak ini perlahan-lahan, alih-alih mengajarkan TLA, kita harus mencuri kebijaksanaan darinya. Sistem tipe banyak meminjam dari Hindley-Milner, dan itu sendiri merupakan pembuktian parsial yang formal
      Saya ingin melihat turunan dari pengujian berbasis properti yang menggunakan teknik SAT atau TLA untuk mempersempit ruang input secara cepat dan dapat diulang. Melalui parsing dan cakupan kode, seharusnya bisa disimpulkan bahwa memberikan 12 ke sebuah fungsi tidak mungkin mengambil cabang yang berbeda dari 11, tetapi nilai seperti -1 atau 2^17 < n < 2^32 mungkin berbeda
    • Argumen “kalau memang berguna, lebih banyak orang pasti sudah memakainya” tidak bagus di bidang apa pun, dan dua kali lebih buruk dalam pengembangan perangkat lunak
      Sampai sekarang sebagian besar proyek perangkat lunak masih gagal. Ini bukan “kegagalan pasar”, melainkan lebih dekat ke “gagal membuatnya” begitu saja

  • Secara garis besar ada dua cabang metode formal. Ada metode ekstrinsik, yang terpisah dari kode itu sendiri dan biasanya menalar spesifikasi kode, serta metode intrinsik, yang masuk ke dalam kode dan menalar kode secara lebih langsung
    Secara historis, metode intrinsik seperti sistem tipe menalar kode pada level fungsi, sementara metode ekstrinsik seperti model checker yang dapat diputuskan seperti Spin/P menangani model kode yang dideskripsikan dengan formalisme seperti automata. Saya melihat masa kini sebagai zaman keemasan riset metode formal, dan dibanding metode intrinsik yang didorong oleh perkembangan sistem tipe serta proyek seperti Verus, metode ekstrinsik tampaknya makin kurang disukai. https://github.com/verus-lang/verus

    • Alat seperti TLA+ bekerja baik karena menargetkan bahasa spesifikasi yang sangat kecil
      Saya pernah melihat pertanyaan tentang bagaimana ini akan bekerja pada bahasa dengan jejak besar seperti Rust, tetapi belum melihat jawaban yang bagus. Saya ingin membaca lebih lanjut
    • Kalau proyek Verus yang ditautkan juga membuat kita menulis spesifikasi kebenaran secara langsung, saya tidak begitu paham mengapa pembedaan itu bermakna
      Kedengarannya seperti mengatakan bahwa metode intrinsik lebih disukai karena tidak perlu menulis dan memelihara spesifikasi terpisah, tetapi kenyataannya tidak begitu

  • Bagian yang membahas metode formal ringan bagus. Memelihara kumpulan strategi proptest di samping codebase bukan investasi yang jauh lebih besar daripada menulis unit test manual, tetapi memberikan wawasan yang jauh lebih baik berkat cakupan yang luas dan contoh kegagalan yang kecil serta mudah dipahami
    Yang terpenting, pendekatan ini juga cocok dengan praktik pengembangan perangkat lunak umum. https://crates.io/crates/proptest

    • Belakangan ini banyak unit test dibuat dengan LLM. Hasilnya cukup bagus, dan kita bisa memintanya agar sedikit lebih menyeluruh, menguji kondisi batas yang terpikir, atau menangani kondisi tertentu
      Saya cukup tahu cara menulis pengujian yang baik dan usaha yang dibutuhkan, tetapi LLM bisa membuat pengujian yang lebih baik jauh lebih cepat daripada saya. Dalam pekerjaan yang repetitif dan membosankan, ia bahkan mungkin tidak semalas saya yang kesabarannya menurun. Sebagai insinyur perangkat lunak, kita semestinya punya refleks untuk mengotomatiskan pekerjaan yang terasa repetitif, dan dokumentasi pun sekarang lebih sering dan lebih dini dibuat karena bisa digenerasi. LLM bisa memicu revolusi kecil dalam adopsi verifikasi formal. Membuat spesifikasi yang benar memang membosankan, tetapi jika ada konteks yang cukup seperti kode yang berjalan, dokumentasi, dan petunjuk, itu mungkin tugas yang relatif mudah bagi LLM. Jika kita bisa meminta spesifikasi dibuat lalu meninjaunya, alih-alih menulis semuanya sendiri, dorongan untuk melakukannya akan jauh lebih besar. Menggunakan Rust juga merupakan sinyal bahwa kita peduli pada kebenaran, dan compiler-nya mendekati alat yang membuktikan bahwa sistem mungkin benar tanpa metode formal. Kemungkinan ini jauh lebih mudah daripada menambahkan metode formal ke bahasa yang bahkan tidak memiliki compiler atau tipe eksplisit
    • proptest atau qcheck bukan metode formal, melainkan pengujian acak

  • Verifikasi formal perangkat lunak masih terlalu sulit digunakan hingga benar-benar bernilai, kecuali untuk kasus-kasus ekstrem. Sebaliknya, verifikasi formal perangkat keras sudah berada pada tingkat yang nyaris tak ada alasan untuk tidak memakainya
    Saya terus mencoba mempelajarinya, tetapi untuk sebagian besar sistem Anda harus menjadi ahli setingkat “orang yang menulis compiler sendiri”. Misalnya, saya mencoba membuktikan encoder/decoder varint; untuk 1–2 byte bisa, tetapi lebih dari itu tidak bisa. Ketika meminta bantuan, ternyata penyebabnya adalah detail internal yang mustahil diketahui, semacam compiler internal hanya meng-unroll loop 5 kali. Belakangan saya belajar Lean dan memang menyukainya, tetapi kemudian bertemu dokumentasi seperti ini: “Definitional equality includes η-equivalence…” dan seterusnya. Saya tidak bermaksud menjelekkan Lean; justru dokumentasinya tampak lebih baik dibanding alternatif lain

    • Penasaran apakah Anda pernah mencoba FizzBee.io. Ia memakai sintaks mirip Python dan contoh-contohnya juga layak dilihat: https://fizzbee.io/examples/two_phase_commit_actors/#complet...
      Metode formal tidak harus rumit. Masalahnya, sebagian besar metode formal dirancang seperti latihan akademis untuk memperlihatkan topik tertentu yang diminati seorang profesor. TLA+ juga lebih dekat ke sesuatu yang dirancang untuk penulisan makalah
    • Kelihatannya menakutkan, tetapi konsep-konsep itu sebenarnya semuanya sangat sederhana, dan kemungkinan besar sudah Anda kenal

  • Salah satu metode formal ringan yang saya sukai, meski tidak terlalu dikenal luas, adalah verifikasi trace menggunakan linear temporal logic: https://en.m.wikipedia.org/wiki/Linear_temporal_logic
    Pada dasarnya Anda hanya perlu mencatat event, dan dalam arsitektur berbasis event, ini praktis bisa didapat gratis. Setelah itu jalankan predikat seperti Always(Locked, Implies(Eventually(Unlocked))) di atas trace eksekusi. Ini juga bisa diterapkan pada trace lama, dan bisa digabungkan dengan stress test atau fuzzing untuk menjelajahi state space. Sederhana, kuat, dapat diterapkan luas, dan hanya membutuhkan predikat tanpa model

    • Ini pembedaan kecil, tetapi karena formula tersebut hanya diperiksa terhadap sebagian subset dari trace sistem, ia lebih dekat ke testing
      Metode formal mengimplikasikan dasar yang komprehensif atas perilaku sistem. Dalam TLA atau sistem sejenis, meskipun yang diperiksa adalah state machine dan bukan sistem nyata, keluarannya adalah bukti bahwa properti LTL/CTL/TLA berlaku untuk semua perilaku sistem, yaitu trace atau pohon trace

  • Diskusi sebelumnya berlangsung pada Juni 2024: https://news.ycombinator.com/item?id=40753989

  • Terlalu lambat. Perencanaan akan segera membatu, dan dokumen apa pun bisa dipakai sebagai bukti yang memberatkan di pengadilan agile

    • Kalau mau diperdebatkan, jika “agile sejati” pernah ditemukan, metode formal akan menjadi kebalikannya. Sebab sesuatu yang dapat dibuktikan dan direproduksi adalah penistaan bagi para penganut sejati

  • Sebagian besar tulisan yang saya baca tentang metode formal terasa seperti lead generation untuk konsultan
    Itu sendiri tidak masalah, tetapi menjengkelkan ketika mereka bersikap seolah sudah mencapai pencerahan lewat metode formal dan menjanjikan bahwa jika saya membeli paket pelatihan untuk karyawan atau kolega, atau mempekerjakan mereka, mereka akan memperbaiki kebiasaan pemrograman yang buruk, bahkan berbahaya secara tidak bertanggung jawab. Kabari saya lagi ketika metode formal benar-benar bisa menghasilkan kode berkualitas tinggi yang tidak mungkin menyimpang dari spesifikasi

    • Bagaimana dengan https://en.wikipedia.org/wiki/SPARK_(programming_language)
    • “Menghasilkan kode berkualitas tinggi yang tidak mungkin menyimpang dari spesifikasi” memang akan berguna, tetapi ada masalah mendasar. Kode terlalu konkret
      Dalam spesifikasi formal, biasanya kita tidak menentukan hingga detail seperti itu, melainkan menentukan perilaku umum sistem. Karena itu, satu spesifikasi sering kali dapat berkorespondensi dengan banyak program yang berbeda secara halus. Ini juga alasan mengapa kode kurang memadai sebagai dokumentasi: kita tidak bisa tahu mana pilihan yang disengaja dan mana yang kebetulan. Kode terlalu konkret untuk menjelaskan requirement tingkat tinggi. Sebaliknya, memverifikasi program terhadap spesifikasi lebih mungkin dapat diimplementasikan

  • Sebagian pendukung metode formal saat ini memandang orang yang tidak memakai metode formal sebagai “malas” atau “bodoh”, dan mencoba mengklaim superioritas karena mereka “melakukan hal yang benar” atau “menguasai bahasa yang rumit”
    Tentu tidak semuanya begitu, dan saya juga mengenal orang-orang baik, tetapi sebagian sebenarnya lebih mirip orang yang hanya punya satu trik. Jika ditanya sistem metode formal lain apa yang mereka pelajari atau coba dalam beberapa tahun terakhir, jawabannya mereka “terlalu sibuk” untuk mempelajari hal baru. Metode formal yang belakangan lebih mudah digunakan antara lain FizzBee, yang memakai dialek Python sehingga terbaca seperti pseudocode; Quint, dengan sintaks yang lebih mudah; dan P, yang sintaksnya akrab bagi pengguna C#. Penulis artikel ini juga pernah menulis bahwa metode formal hanya menyelesaikan separuh masalahnya: https://brooker.co.za/blog/2022/06/02/formal.html
    Namun masalah yang disebutkan di sana sudah diselesaikan oleh PRISM, yang bahkan bukan hal baru. Brooker saja yang tidak mau mencari-cari atau belajar di sekitarnya