- Sejarah formalisasi matematika tidak dimulai dengan Lean, dan selama hampir 60 tahun berbagai keluarga sistem sudah lebih dulu mengumpulkan teknik inti dan hasil penting
- Alat seperti AUTOMATH pada 1968, keluarga LCF, HOL, Rocq, ACL2, dan Mizar telah menghasilkan formalisasi luas, dari analisis real hingga teorema bilangan prima, teorema empat warna, dan dugaan Kepler
- Lean membangun definisi matematika modern dengan cepat berkat pustaka besar dan komunitas yang aktif, tetapi propositions as types maupun tipe dependen bukan satu-satunya jalan bagi proof assistant
- Isabelle menonjolkan otomatisasi yang kuat, keterbacaan tinggi, dan penghindaran tipe dependen, sambil meneruskan tradisi LCF yang menyusun pemeriksaan bukti lewat penghalang abstraksi kernel tanpa proof object
- Dengan AI yang juga mulai merapikan bukti terstruktur dan menerjemahkannya ke sistem lain, beban untuk memandang satu alat sebagai standar mutlak mungkin akan makin berkurang ke depan
Sistem awal dan garis keturunan lain
-
AUTOMATH
- AUTOMATH sudah memuat hampir semua unsur yang diperlukan untuk formalisasi matematika pada 1968
- Pada 1977, Jutting memformalisasikan Foundations of Analysis karya Landau dengan AUTOMATH, dan membahas dari logika murni hingga konstruksi bilangan kompleks
- Ia menggunakan kelas ekivalensi dan himpunan bilangan rasional, serta membuktikan secara formal kelengkapan Dedekind dari garis bilangan real
- Pencapaian ini tidak terulang selama 20 tahun, dan baru pada pertengahan 1990-an formalisasi bilangan real kembali dilakukan lewat HOL Light milik John Harrison dan Isabelle/HOL milik Jacques Fleuriot
- Notasinya sangat tidak nyaman dan tidak memiliki otomatisasi sama sekali, sehingga buktinya panjang dan sulit dibaca
- Meski begitu, untuk menangani kelas ekivalensi sistem ini dinilai lebih baik daripada Rocq; berbeda dengan setoid hell yang dialami pengguna Rocq, Jutting dapat memformalisasikan kelas ekivalensi dengan tenang
-
Boyer dan Moore
Arus setelah LCF
- Edinburgh LCF berfokus pada teori bahasa pemrograman, tetapi gagasan menjadikan bahasa fungsional sebagai metalanguage untuk proof assistant menyebar luas
- Berbagai kelompok di Cambridge, INRIA, Cornell, dan tempat lain memakai ML untuk membuat alat awal seperti HOL, Coq (kini Rocq), dan Nuprl
- Kelompok HOL berfokus pada verifikasi perangkat keras, tetapi verifikasi perangkat keras floating-point membuat analisis real menjadi diperlukan
- John Harrison membuktikan hasil matematika yang serius seperti teorema bilangan prima dalam keluarga HOL melalui rumus integral Cauchy
- Di bawah tujuan untuk memverifikasi sebanyak mungkin dari 100 theorems, HOL Light sering berada di peringkat teratas
- Hingga 2014, sistem-sistem dalam garis keturunan ini telah memformalisasikan berbagai teorema tingkat lanjut
- Teorema-teorema ini umumnya memiliki bukti yang panjang dan kompleks, dan pekerjaan formalisasinya juga sangat besar, sekaligus berperan penting dalam mengurangi keraguan yang tersisa pada teorema-teorema tersebut
Kebangkitan komunitas Lean
- Para matematikawan menilai pencapaian formalisasi sebelumnya belum menjangkau konstruksi rumit dalam matematika modern arus utama seperti Grothendieck schemes atau perfectoid spaces
- Tom Hales memilih arah membangun definisi-definisi ini sebagai pustaka, dengan fokus pada akumulasi definisi ketimbang bukti, dan memilih Lean
- Ia mempresentasikan arah ini dalam program Big Proof, dan gagasan serupa juga dibahas di sana
- Setelah Kevin Buzzard mendengar hal ini dan memutuskan mencoba Lean untuk pendidikan, penyebarannya kemudian melaju cepat
- Sebagai titik balik penting bagi komunitas Lean, ditunjukkan bahwa ia lepas dari obsesi terhadap bukti konstruktif yang lama mendominasi Rocq
- Intuisionisme muncul setelah paradoks Russell dan memiliki implikasi tertentu juga terhadap konsep bilangan real
- Martin-Löf type theory jelas merupakan formalisme yang intuisionistis, tetapi Rocq disebut tidak bisa dipandang sesederhana itu
- Meski demikian, dalam makalah-makalah terkait Rocq, bukti konstruktif terus berulang bahkan di tempat yang tidak relevan atau tidak bermakna, dan kecenderungan ini dianggap menghambat penerapan matematika Rocq sambil menyerahkan posisi itu kepada Lean
propositions as types dan perbedaan dengan LCF
- Propositions as types adalah dualitas yang menghubungkan simbol logika ∀, ∃, →, ∧, ∨ dengan pembentuk tipe Π, Σ, →, ×, +
- Kerangka ini indah dan produktif secara teoretis, tetapi bukan satu-satunya jalan
- Jika proof assistant dibatasi menjadi perangkat lunak yang memeriksa bukti dengan prinsip propositions as types, maka sebagian besar penelitian setengah abad terakhir terdorong keluar dari definisi
- Dengan begitu hanya Rocq, Lean, dan Agda yang tersisa
- Bahkan AUTOMATH bukan contoh propositions as types; meski ada unsur mirip Π dan →, logikanya tetap ditetapkan sebagai aksioma seperti dalam buku teks logika umum
- Lima puluh tahun lalu de Bruijn sudah menganggap pemisahan tipe dan proposisi itu perlu
- Contoh yang diberikan: pembagian harus menerima tiga argumen, dan nilai dari (x/y) akan bergantung pada bukti bahwa (y \ne 0), sehingga diperlukan proof irrelevance
- Juga ditegaskan bahwa anggapan bahwa pendekatan LCF sama dengan propositions as types tidak sesuai fakta
- Rocq dan Lean memiliki Prop sebagai sort untuk proposisi; di sini semua objek bukti dari proposisi yang sama dievaluasi sebagai nilai yang sama, sehingga memberi proof irrelevance
- Namun itu tidak membuat proof object raksasa lenyap; dalam sistem nyata mereka tetap ada
- Temuan inti Robin Milner justru bahwa dalam LCF proof object itu sendiri tidak diperlukan
- Jika kernel bukti ditempatkan di dalam abstract data type milik ML dan aturan inferensi dijadikan konstruktor, maka bukti dapat diperiksa secara dinamis
- Berkat abstraction barrier di ML, kecurangan dianggap mustahil
- Di era RAMmageddon, keberadaan term raksasa yang tidak menunjukkan apa-apa namun tetap memakan puluhan MB terasa sangat tidak rasional
- Dikritik juga bahwa bahkan ada penelitian yang berlanjut untuk membuat term-term tak perlu seperti itu tampak lebih elegan
Alasan memilih Isabelle
- Jika rekan-rekan memakai Lean, keahlian tim juga ada di Lean, dan pustaka prasyarat yang diperlukan pun ada di Lean, maka memilih Lean tentu terasa wajar
- Namun jika bisa memilih dengan bebas, tetap ada alasan jelas untuk mempertimbangkan Isabelle
-
Otomatisasi
- Keunggulannya disebut sebagai otomatisasi paling kuat, dan bahkan dibandingkan “hammer” sehari-hari, tidak ada yang dinilai sebanding dengan sledgehammer
- Disebut juga bahwa sisi aljabar komputer perlu dibahas secara terpisah
-
Keterbacaan
-
Menghindari tipe dependen
- Karena tidak memiliki tipe dependen, ia menghindari universe level dan berbagai keanehan lain yang menyulitkan pemula
- Dituliskan pula bahwa di mathlib milik Lean serta SSReflect dan Mathematical Components milik Rocq, penggunaan tipe dependen juga tidak dianjurkan
- Kesulitan inti tipe dependen adalah bahwa jika diimplementasikan dengan benar, pengecekan tipe itu sendiri menjadi tak terputuskan
- Alasannya karena penentuan kesetaraan juga tak terputuskan, dan pada masa awal hal ini dianggap wajar
- Sejak sekitar 1990, konsensus bergeser ke arah membuat pengecekan tipe dapat diputuskan dengan menurunkan kesetaraan menjadi definitional/intensional equality
- Akibatnya, (T(N+1)) dan (T(1+N)) menjadi dua tipe yang berbeda
- Batasan seperti ini memengaruhi bukti nyata, dan pemeriksaan definitional equality sendiri tetap membawa beban komputasi yang besar
Matematika modern tanpa tipe dependen pun memungkinkan
- Dituliskan bahwa pada 2017, pandangan tentang seberapa jauh Isabelle bisa menangani matematika masih jauh lebih hati-hati
- Saat itu, topik-topik seperti berikut mudah terlihat seolah benar-benar memerlukan tipe dependen
- Namun lewat riset terkait Alexandria, banyak hal dipelajari, dan intinya diringkas sebagai jangan memaksakan semuanya masuk ke tipe
Arah ke depan dan AI
- Lean telah mengambil banyak keputusan yang tepat dan bahkan mendukung blok bukti bertingkat, sehingga berpotensi menjadi bahasa bukti yang cukup mudah dibaca
- Kini komunitas Lean perlu benar-benar memanfaatkan kemampuan itu, sementara pengguna Isabelle disebut umumnya sudah melakukannya
- Yang lebih penting daripada proof object yang bisa diperiksa komputer adalah kejernihan teks bukti yang benar-benar bisa dibaca manusia
- Kebangkitan AI membuat perbedaan ini makin jelas
- Bukti buatan AI sering kali berantakan, tetapi mudah dirapikan dengan sledgehammer, dan jika strukturnya tertata baik, detail yang berlebihan pun masih dapat dibaca
- Dengan begitu, alur pengerjaan lebih mudah dipahami dan lebih mudah pula dipangkas menjadi bentuk yang lebih sederhana
- Baru-baru ini juga muncul riset tentang model bahasa yang secara langsung memanggil sledgehammer
- AI juga dapat dengan mudah menerjemahkan bukti terstruktur yang mudah dibaca dari satu proof assistant ke proof assistant lain
- Jika demikian, beban dalam memilih sistem mana yang akan dipakai itu sendiri akan berkurang
Melengkapi kelalaian tentang Mizar
- Sejarah formalisasi matematika tidak akan lengkap tanpa Mizar dan pustaka matematikanya yang sangat besar
- Bahasa Isar milik Isabelle juga banyak dipengaruhi oleh Mizar
- Kelalaian karena tidak menyebut Mizar diperbaiki secara khusus, dan disebutkan bahwa tulisan berikutnya akan membahas Mizar
1 komentar
Pendapat Hacker News
Kebanyakan pembaca HN lebih dekat ke programmer daripada matematikawan, jadi melihat Lean dari sudut pandang pemrograman terasa lebih praktis daripada dari sisi pembuktian matematika
Sebagai buku yang membahas Lean dari perspektif pemrograman fungsional, https://leanprover.github.io/functional_programming_in_lean/ cukup bagus
Saya juga sedang belajar Lean jadi mungkin masih punya pandangan terlalu optimistis sebagai pemula, tetapi tujuan saya adalah menulis dan membuktikan kode programmer biasa seperti algoritme kompresi/dekompresi nyata, seperti contoh lean-zip belakangan ini
https://github.com/kiranandcode/lean-zip/blob/master/Zip/Nat...
https://github.com/dharmatech/symbolism.lean
Ini port dari kode C#, dan daya ekspresif Lean luar biasa besar
Saya pernah melihatnya sempat cukup ramai dibicarakan, tapi belakangan tidak terlalu mengikuti bidang ini secara detail
Lalu saya melihat dua hambatan lagi. Pertama, mengetahui apa yang harus dilakukan perangkat lunak itu sendiri sudah sulit, dan apa yang ingin dilakukan pengguna belum tentu sama dengan hal yang dibayar pelanggan
Kedua, kualitas kerja banyak pengembang begitu rendah sehingga sulit berharap mereka akan lebih mahir menangani bahasa kebenaran daripada bahasa seperti Java
Namun yang kedua ini bisa saja hilang jika digantikan sistem AI yang memberi perhatian yang diperlukan, dan kalau itu terjadi situasinya mungkin berubah
Menurut saya, seperti halnya matematika yang sudah ditinggalkan pemrograman fungsional, itu juga tidak terlalu relevan bagi kebanyakan programmer
Penulis tampaknya cukup salah paham soal Lean, dan itu justru lebih mengejutkan karena ia terlihat seperti orang yang paham bidang ini
Ia tampaknya menganggap Lean mempertahankan objek bukti apa adanya lalu pada akhirnya memeriksa satu objek bukti raksasa dengan semua definisi di-expand, padahal kenyataannya jauh dari itu
Lean pada dasarnya mengimplementasikan optimisasi yang dipuji penulis sebagai kelebihan LCF dengan cara yang hampir sama. Analogi kasarnya, seperti menghapus papan tulis sambil melanjutkan pembuktian
Di Lean4, jika ditulis dengan
theoremalih-alihdef, objek buktinya tidak dipakai lagi, dan ini bukan sekadar optimisasi, melainkan sifat inti bahasa. theorem bersifat opaqueKalaupun term bukti masih tersisa, itu hanya agar pengguna bisa melihatnya dalam mode interaktif, dan kernel bahkan tidak bisa peduli apa isi objek bukti itu
Dalam LCF, bukti dan term itu berbeda, dan menurut saya memang seharusnya begitu. Kebingungan ala Curry-Howard seperti ini tidak perlu, tetapi banyak orang mengira itulah satu-satunya cara melakukan matematika dengan komputer
Kalau mau, di LCF pun bukti bisa disimpan dan dimanfaatkan, dan di Lean pun kalau mau bisa dihilangkan lewat optimisasi
Pendekatan tipe abstrak mungkin menghemat memori sedikit, tetapi hanya beda faktor konstan dan bukan perbaikan asimtotik
Keluhan bahwa Lean membuang-buang puluhan MB mungkin penting pada 1980-an atau 1990-an, tetapi sekarang sepertinya bukan lagi keunggulan yang begitu menentukan
Saya sering mendengar Lean bagus untuk pemrograman fungsional, tetapi kalau datang dari Agda rasanya seperti downgrade yang cukup kikuk
Tactic-nya juga dibilang bagus, tetapi dalam pengalaman saya tactic Coq lebih kuat dan lebih nyaman dipakai
Mungkin ini semua cuma bias kesan pertama, tetapi sejauh ini kekuatan Lean tampaknya bukan karena ia paling unggul dalam satu hal, melainkan karena secara keseluruhan cukup baik dan komunitasnya besar
Saya paham kenapa itu menarik, tetapi sayang juga rasanya karena ada sedikit keindahan dan kekuatan yang hilang sebagai gantinya
Namun efek seperti ini sering tampak abadi pada saat itu, padahal kenyataannya tidak selama yang dibayangkan. Kalau memang hanya itu yang penting, Perl seharusnya masih tetap raksasa sampai sekarang
Di Lean, yang terutama besar pengaruhnya adalah mereka lebih dulu punya library besar. Mirip seperti peran CPAN bagi Perl
Tetapi kalau melihat hukum penskalaan, bagi kebanyakan pengguna nilai library besar kemungkinan hanya bertambah kira-kira sebesar log dari ukurannya
https://pdodds.w3.uvm.edu/teaching/courses/2009-08UVM-300/do...
Di awal jurang ini tampak mustahil dikejar, tetapi tanpa harus mengejar skala yang sama pun, pada titik tertentu kemudahan pakai menjadi lebih penting
Selain itu, porting library matematika juga cocok untuk LLM. Sumbernya sudah terverifikasi, targetnya juga bisa diverifikasi, dan jalur penalarannya umumnya bisa dipindahkan
Sebaliknya, ini berarti berkat LLM hambatan bekerja di platform kecil juga lebih rendah dari perkiraan. Jika saya bisa memindahkan library mereka ke platform saya, besar kemungkinan pembuktian saya juga bisa dipindahkan ke sana
Alat yang sempurna bukan inti persoalannya; yang lebih penting adalah menyelesaikan pekerjaan dengan alat yang cukup bagus
Lean tampaknya punya ruang untuk berkembang sebagai bahasa fungsional untuk pengembangan perangkat lunak, sampai-sampai benar-benar bisa menjadi penerus Haskell
Perbedaannya terutama terasa pada dukungan tooling. Dokumentasi Agda kurang bagus, memasangnya dan menjalankannya di sistem juga merepotkan, dan secara praktis sangat mendorong penggunaan Emacs
Sebaliknya, Lean bahkan punya panduan menulis utilitas
catdalam dokumentasi resminya, dan secara umum memberi pengalaman tooling yang jauh lebih modernBiasanya pujian banyak saya dengar pada dependent pattern matching, dan di bagian itu Lean memang terasa cukup lemah
Tetapi kalau dalam FP umum pun Agda terasa lebih ramah, saya ingin tahu di aspek mana
Isabelle/HOL bahasanya sendiri lumayan, tetapi tooling-nya punya cacat mendalam bahkan di luar pendekatan yang berpusat pada desktop
Bahasanya tidak benar-benar lebih baik dari Lean, hanya berbeda, dan saya setuju dengan beberapa kritik terhadap tipe dependen
Pada akhirnya kedua bahasa itu membuat trade-off yang berbeda, dan pilihan itu tampaknya membuat masing-masing menjadi alat yang cukup efisien di wilayahnya. Ranah pembuktian sendiri begitu luas sehingga tiap paradigma punya kekuatan dan kelemahannya, dan Lean hanya terspesialisasi di bagian yang berbeda
Sledgehammer bagus, tetapi rasanya tinggal soal waktu sampai Lean punya sesuatu yang serupa
Pada tahap eksplorasi itu bisa berguna, tetapi boros sumber daya, dan meski bisa membuat bukti lebih singkat, untuk kode yang dipublikasikan saya lebih suka seluruh langkah bukti terlihat jelas daripada
by sledgehammeryang setengah terasa seperti sihirSebaliknya, mengembangkan Isabelle sendiri jauh lebih menyakitkan daripada Lean, terutama dalam berkomunikasi dengan para pengembangnya
Sikap di mailing list seperti tidak ada bug, yang ada hanya perilaku tak terduga terlihat kekanak-kanakan dan tidak profesional
Dan mengejek penggunaan RAM sistem mirip Lean juga cukup lucu kalau melihat rakus memorinya Isabelle sendiri
Praktis tingkat kesulitannya hampir sama dengan menggunakan bukti formal itu sendiri
Mungkin saya tertukar dengan HOL lain
grinddi Mathlibhttps://leanprover-community.github.io/mathlib4_docs/Init/Gr...
Hal menarik dari Lean adalah Lean itu bahasa, tetapi yang paling sering dibicarakan orang sebenarnya adalah library bernama Mathlib
Para pembuat Mathlib tampak cukup pragmatis, sehingga mereka memasukkan logika klasik ke dalam tipe Lean dan hanya memakai sebagian logika intuisionistik
“Sesuatu tidak bisa sekaligus benar dan salah” bukanlah hukum tertium non datur, melainkan hukum nonkontradiksi
Hukum tertium non datur berarti
pbenar ataunot pbenarhttps://en.wikipedia.org/wiki/Law_of_noncontradiction
https://www.cslib.io https://www.github.com/leanprover/cslib
Logika intuisionistik pada dasarnya bermakna sebagai upaya mengubah argumen matematika menjadi konstruksi yang dapat dihitung, jadi menarik melihat bagaimana mereka akan menangani persoalan ini
Sebenarnya begitu menulis algoritme di Lean, kita sudah masuk ke semacam batasan konstruktif dalam bentuk apa pun, dan untuk tujuan itu mungkin tingkat logika seperti itu sudah cukup
penyangkalan, kemarahan, tawar-menawar, depresi, penerimaan
Kuliah dan tulisan terkait dari Andrej Bauer juga layak dilihat
https://www.youtube.com/watch?v=21qPOReu4FI
http://dx.doi.org/10.1090/bull/1556
Menurut saya tulisan seperti ini perlu lebih banyak
Terhadap pola pikir kelompok yang seolah semuanya sudah jelas dan tinggal mendorong pokoknya pakai X, selalu ada alasan yang cukup meyakinkan untuk setidaknya meninjau alternatif
Walaupun akhirnya tetap meninggalkan alternatif dan memilih arus utama, menurut saya lebih baik memilih sambil memahami medannya
Bahkan sekarang kita sudah membuat terlalu banyak framework dan alternatif, mungkin juga karena itu menyenangkan
Alih-alih memperbaiki alat yang ada atau sekadar menyelesaikan pekerjaan nyata, kita sering terus menambah bahasa, library, dan build tool tanpa henti
Menurut saya justru akan lebih baik jika jumlah bahasa, library, dan build tool sekarang hanya setengahnya
Semakin jauh dari arus utama, dokumentasi makin sedikit, bug makin banyak karena sudut yang kurang dijelajahi, dan orang yang bisa dimintai bantuan makin sedikit
Kalau pilihan sudah menumpuk lebih dari dua puluh, secara rata-rata memang lebih masuk akal memilih opsi standar lalu lanjut. Perhatian itu terbatas; kalau harus menulis laporan investigasi untuk tiap dependensi, masalah inti justru tidak terselesaikan
Ada dua pengecualian, yaitu ketika alat standar benar-benar tidak cocok dengan use case saya, atau ketika alat standar itu sendiri sangat tumpang tindih dengan masalah inti yang ingin saya pecahkan
Diskusi seperti ini terasa mirip dengan tulisan-tulisan yang menyoroti keterbatasan Python untuk komputasi ilmiah
Begitu sebuah komunitas berkumpul melewati massa kritis di sekitar alat yang lumayan baik, itu mengalahkan hampir semua faktor lain
Momentum muncul, tutorial, tulisan penjelas, dan dokumentasi yang lebih baik menumpuk, hingga praktis mencapai escape velocity
Lean tampaknya tepat berada di posisi itu sekarang, apalagi dengan pendukung kuat seperti Terrance Tao
Jadi, pernyataan bahwa “bahasa X lebih baik” tidak sepenuhnya salah, tetapi mudah meleset dari pertanyaan yang sebenarnya penting
Kuncinya adalah apakah itu benar-benar lebih baik daripada alat yang semua orang sudah kenal, bisa langsung dipakai, dan terus menerima lebih banyak waktu untuk perbaikan
Pada akhirnya ini terlihat seperti situasi worse is better, atau bahwa bagus dan populer saja sudah cukup
Terutama karena di bidang ini hasil terjemahannya bisa diverifikasi otomatis sampai tingkat yang cukup tinggi, sehingga pilihan platform itu sendiri mungkin bukan masalah besar
AI bisa menulis kode sendiri meski tidak ada library komunitas raksasa, dan bisa membaca dokumentasi serta spesifikasi langsung tanpa perlu sejuta tutorial beredar di internet
Tidak perlu menghindari bahasa yang tak punya pasar kerja. AI tidak sedang membangun karier; ia hanya perlu mengerjakan tugas yang ada saat itu
Karena itu, bahasa kecil dan DSL yang dulu hampir tidak punya peluang kini lebih mungkin diadopsi
Monokultur bahasa yang bertahan lama dalam pemrograman pun bisa saja diakhiri oleh AI
Pernyataan bahwa “hampir semua yang diformalisasikan dengan sistem apa pun hari ini mungkin juga bisa diformalisasikan di AUTOMATH” mirip dengan mengatakan bahwa apa pun yang ditulis dengan bahasa modern saat ini juga bisa ditulis dengan assembly 50 tahun lalu
Secara teknis benar, tetapi secara ekonomi sama sekali berbeda
Sekitar 15 tahun lalu saya sempat mencoba Coq/Rocq dan beberapa alat lain, dan yang sulit dipahami bukan hanya konsepnya, tetapi perangkat lunaknya sendiri
Hal aneh pada proof assistant / interactive theorem prover adalah bahwa karena sifatnya interaktif, bentuknya menjadi gabungan bahasa dan IDE, dan dalam praktiknya keduanya terikat kuat
Karena itu sulit membicarakan bahasanya secara terpisah; kita juga harus melihat lingkungan tempat ia dipakai
Saya juga bukan penggemar berat VS Code, tetapi jelas bahwa IDE yang dapat diperluas dan dipakai begitu banyak orang, dengan investasi besar dan pemolesan yang matang, jauh lebih unggul daripada lingkungan alternatif
Jalur masuk yang bagus seperti Natural Numbers Game tampaknya juga dimungkinkan oleh kemampuan VS Code untuk di-hack dan oleh ekosistemnya
Namun saat belajar Lean, yang saya khawatirkan adalah ekstensibilitas sintaks sebagai pedang bermata dua
Setelah mempelajari sebuah bahasa, orang ingin bisa membaca kode yang ditulis dengannya, tetapi kalau tiap proyek mulai membuat DSL-nya sendiri dalam jumlah besar, itu bisa tak terkendali
Pada akhirnya ini bergantung pada seberapa menahan diri komunitas dan ekosistemnya, jadi saya melihatnya dengan campuran harap dan khawatir
Lean bukan proof assistant yang paling dicintai matematikawan, dan juga bukan alat yang paling cocok untuk verifikasi formal perangkat lunak
Tetapi ia lumayan mampu melakukan keduanya, dan sebagai gantinya berhasil menangkap momentum yang paling sulit didapat
Ditambah lagi, di era AI jumlah kode buatan manusia yang tersedia secara publik langsung memengaruhi seberapa baik agen dapat menghasilkan kode baru, sehingga momentum itu menjadi makin kuat