Tulisan yang bagus. Dari sudut pandang seseorang yang dulu pernah melakukan verifikasi program, Rust tampak seperti bahasa modern yang paling berguna untuk menerapkan teknik formal
Aturan Rust menghilangkan banyak kasus yang sulit diformalkan. Masalah besar yang tersisa adalah analisis deadlock dari perspektif thread dan perspektif Rc/borrow, dan keduanya sampai batas tertentu setara. Jika Rust memiliki analisis deadlock statis, tampaknya pointer dereference yang aman juga bisa dimungkinkan, dan jika dapat dibuktikan bahwa semua pemanggilan borrow/upgrade tidak gagal, sebagian besar reference count bisa dihapus. Dengan begitu, jika memungkinkan, mutabilitas internal juga bisa didapatkan secara gratis
Masalah besar theorem prover adalah karena dibuat oleh orang-orang yang suka membuktikan teorema, mereka cenderung terjebak dalam formalisme sehingga rasa UI dan programmer-nya melenceng. Sebagian besar kewajiban pembuktian dapat ditangani dengan SAT solver, tetapi masalah yang sulit membutuhkan alat yang lebih berat. Coq terlalu manual, dan penulis menganggap ACL2 terlalu fungsional. Machine learning bisa membantu mengarahkan theorem prover. Sulit menyerahkan pembuktian itu sendiri, tetapi tampaknya mungkin untuk menyimpulkan rencana pembuktian pada kode yang alur kontrol dan penggunaan datanya umumnya mirip
F* mendekati bahasa mitos yang membuktikan secara otomatis. Ia memakai SMT solver yang lebih kuat daripada SAT, dan jika penyelesaian otomatis gagal, pembuktian manual juga dimungkinkan
Rutin kriptografi Firefox dan Wireguard ditulis bukan dalam Rust, melainkan F*, lebih tepatnya Low*, DSL tingkat rendah yang tertanam di F*, dan telah diverifikasi sepenuhnya https://project-everest.github.io/ https://mitls.org/
Setuju, tetapi menurut saya Lean sedang membuat kemajuan besar dalam pengalaman pengguna untuk verifikasi theorem proving interaktif berkat fitur metaprogramming yang kaya
Masalah saat menerapkan alat seperti ini untuk memverifikasi bahasa eksternal seperti Rust adalah pembuktian tidak ditulis dalam bahasa target, sehingga developer harus mempelajari dua bahasa. Berdasarkan pengalaman menulis Creusot, pekerjaan pada Verus dan Aeneas, serta pengalaman di laboratorium Why3, saya telah memikirkan seperti apa “Rust yang sadar verifikasi” itu. Jika bahasa seperti itu dibuat dari awal, kemudahan verifikasinya bisa meningkat secara bertahap bahkan dibanding Rust, dan tampaknya akan sangat efektif terutama pada bagian pembuktian yang sulit
Saya rasa keluarga Coq/Agda/Lean akan menjadi pemenang di bidang pembuktian. Interaksi adalah model yang cukup baik sebagai loop umpan balik, dan sistem-sistem ini sudah ada serta benar-benar berfungsi
Fitur bawaan yang paling saya rasa kurang adalah sesuatu seperti “jalankan quickcheck pada bukti saya”. Ketika ada kode dan kita mencoba membuktikan properti yang ternyata tidak benar, mudah sekali pusing memikirkan kenapa buktinya tidak jalan. Saat di tengah pembuktian kita mencapai keadaan yang tidak masuk akal, akan menyenangkan jika ada perintah seperti “coba buat counterexample di sini” yang mengeluarkan counterexample. Pembuktian sangat bergantung pada jalur dan umumnya tidak mudah, tetapi alat-alat ini tampak sangat dekat dengan kehebatan. Proses mencoba membuktikan kode juga harus mencerminkan kemungkinan bahwa kode itu bisa memiliki bug
Gagasan bahwa machine learning memandu theorem prover itu menarik. Jika sistem machine learning benar, ia menuntun ke bukti yang valid dan memberi keuntungan besar; jika salah pun kerugiannya tidak besar
Prover tidak menghasilkan bukti yang salah, ia hanya gagal menghasilkan bukti yang valid. Menurut saya tidak banyak penerapan machine learning yang memiliki sifat seperti ini
Saya bukan ahli verifikasi formal, tetapi menurut saya lock dalam arti tradisional tidak banyak membantu. Tidak ada compiler yang memberi sesuatu yang benar-benar berguna soal lock, jadi kita hanya harus menerima risikonya dan hidup dengannya
Sebenarnya di Rust, lock dan reference count adalah struktur runtime. Arc sangat merusak model RAII Rust, sehingga scoped thread yang destruktornya harus berjalan sebelum scope berakhir harus dihapus. Reference count global punya masalah siklus dan kebocoran, dan kembali menjadi masalah global. Mungkin sulit menghilangkannya sepenuhnya, tetapi saya percaya lebih baik mengurungnya dalam scope bergaya arena. Untuk lock, tampaknya diperlukan struktur data asimetris seperti channel. Di Go, channel dibagi menjadi sender dan receiver, dan di goroutine pengirim kita bisa memasang defer close(ch), yang dijamin dieksekusi setelah sisa thread selesai bahkan jika terjadi panic. Tidak harus channel, tetapi memisahkan peran baca-tulis/produsen-konsumen akan membuat penalaran jauh lebih mudah dan tampaknya juga membantu analisis formal
Saya suka bagaimana ini dimulai dari kutipan makalah Hoare sekitar 1973 dan kini berlanjut sampai tulisan kedua. Awalnya saya menulis komentar panjang di thread HN untuk tulisan boat, mengatakan bahwa memiringkan kutipan itu ke sudut pandang yang berpusat pada Rust bisa dimengerti mengingat latar belakang boat, tetapi itu mempersempit cakupan kritik Hoare secara artifisial
Sekarang Grayson menjadikan potongan sempit itu sebagai titik awal untuk membahas beberapa wilayah dan titik desain Rust yang menarik. Saya masih merasa komentar saya benar, tetapi diskusi yang berlanjut dari tulisan Grayson sudah cukup untuk menutupi keberatan teknis saya terhadap tulisan yang menjadi titik awalnya
Sekitar pertengahan 1990-an, Hoare sendiri tampaknya sudah menyadari bahwa mungkin ada sesuatu yang keliru pada dasar pendekatan berpusat pada soundness ala 1970-an: http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h...
Setelah itu, dengan munculnya teknik-teknik unsound yang lebih maju daripada sekadar pengujian sederhana, menurut saya metode unsound justru melangkah lebih jauh daripada metode sound
Tahun 1973 itu 50 tahun lalu, setara dengan satu masa hidup seorang ahli. Hoare benar-benar sudah sangat dekat
Ia menemukan masalahnya, dan jika dilihat ke belakang, solusi memaksakan sharing XOR mutability melalui sistem tipe tampak seperti satu langkah kecil. Seandainya saat itu orang menyadari bahwa langkah kecil itulah solusinya, penderitaan luar biasa selama 50 tahun bisa berkurang
Inilah pemikiran yang semula saya tulis tentang kutipan makalah Hoare oleh boat. Setelah kutipan pertama Hoare dan pengantar singkat, penulis mengatakan, “ketika Tony Hoare mengatakan bahwa referensi itu seperti jump, yang ia bahas adalah masalah state yang mutable dan memiliki alias.” Karena withoutboats adalah pengembang Rust terkenal, interpretasi seperti ini tidak mengejutkan
Namun saya tidak melihat kutipan itu sendiri memperkuat sudut pandang tersebut. Bisa dilihat sebagai upaya mengambil keluhan Hoare yang lebih umum tentang keberadaan semantik referensi itu sendiri, lalu menerapkannya pada model state mutable tanpa alias milik Rust untuk menghindari masalah. Namun ini lebih mirip memperbaiki hanya potongan sempit dari masalah yang lebih besar lalu mengatakan seluruh masalahnya sudah hilang. Bagian-bagian yang hilang, khususnya awal bagian “Variables” dan contoh ALGOL 68, jauh lebih kuat mengarah pada bahwa Hoare mengkritik konsep semantik referensi itu sendiri, bukan sekadar state mutable. Saya mengakui Rust adalah upaya untuk menjinakkan sebagian masalah, tetapi saya tidak melihat ada bahasa mana pun yang telah “memperbaiki” masalah ini
Saya tidak begitu mengerti mengapa tulisan ini mendapat begitu banyak pujian. Rasanya seperti menyapu berbagai bidang analisis program dalam satu paragraf. Saya menyukai Graydon dan menghormati sudut pandangnya, tetapi paragraf ini terlalu menyederhanakan
Penjelasan seolah-olah bahasa dengan GC sengaja tidak memiliki dukungan kuat untuk penalaran lokal adalah strawman. Ada bahasa seperti Pony yang memakai GC sambil tetap menempatkan region di sistem tipenya. Selain itu ada seluruh bidang analisis pointer dan analisis escape, yang menginfer keunikan dan menentukan apakah dua referensi mungkin menjadi alias. Inti dari tipe statis juga adalah membagi heap menjadi bagian-bagian yang tidak saling ber-alias melalui teknik seperti class dan field. Ini bukan soal JavaScript, dan kita tidak boleh berpura-pura bahwa Java/C#/Scala serta banyak bahasa GC tidak memiliki penalaran lokal atas state mutable
Dalam kasus umum, ini tidak bisa sepenuhnya dilakukan otomatis, dan pada praktiknya diperlukan sesuatu yang cukup mirip dengan separation logic. Semantik borrow checker Rust juga bisa dilihat sebagai semacam separation logic yang disederhanakan
Class dan field tidak menyediakan penalaran lokal penuh atas state mutable. Sebab class/objek A bisa saja bergantung pada state mutable class/objek B. Pewarisan class ala Java dengan sendirinya menambahkan lebih banyak kompleksitas seiring program berevolusi dari waktu ke waktu
Graydon tidak mengatakan bahwa GC membuat penalaran lokal yang kuat menjadi mustahil. Ia mengatakan bahwa, apa pun alasannya, sebagian besar perancang bahasa membuat pilihan yang berlawanan dengan tujuan itu, dan itu tampak jelas benar
Tentu ada contoh tandingan, tetapi jika melihat bahasa GC serbaguna arus utama seperti Java, C#, dan Python, pernyataan itu benar. Bisa ditafsirkan bahwa gagasan awal object-oriented lebih dekat dengan actor model saat ini, dan dimaksudkan untuk mengubah struktur data yang dimiliki hanya lewat pengiriman pesan. Namun implementasi object-oriented di dunia nyata hampir tidak mendekati tujuan itu. Java tidak mencegah penyimpanan referensi mutable ke objek yang sama di banyak objek. Tulisan ini menjelaskan poin itu dengan lebih baik: https://without.boats/blog/references-are-like-jumps/
Sebagai kuis sederhana, apa yang dicetak kode ini? void myMethod(final Map map) { map.remove("key"); int oldSize = map.size(); map.put("key", "val"); int newSize = map.size(); System.out.println(newSize - oldSize); }
Edit: saya salah membaca negasi ganda. Bahkan setelah dibaca ulang, tetap membingungkan. Maksudnya Java memiliki penalaran lokal, tidak seperti JavaScript?
Biasanya saya menyukai tulisan Graydon, tetapi tulisan ini, seperti banyak tulisan tentang teknik formal, bisa menyesatkan pembaca yang tidak mengenal bidangnya. Ini mirip dengan mengatakan bahwa cara mengubah timbal menjadi emas sudah meningkat beberapa orde satu digit, tetapi tidak mengatakan bahwa masih tersisa 29 orde lagi sebelum efisiensi biaya praktis tercapai
Apakah tidak adanya alias sangat memudahkan verifikasi formal? Ya. Tetapi apakah itu berarti program dunia nyata dapat diverifikasi secara praktis dan hemat biaya? Sama sekali tidak. Ada program, sirkuit, dan komponen yang diverifikasi secara formal setiap hari, tetapi itu lebih merupakan pengecualian, relatif sangat kecil, dan dibuat dengan cara yang sangat hati-hati. Properti yang membantu penalaran lokal memang penting, tetapi tidak memberi perubahan nyata pada cara menjamin kebenaran perangkat lunak arus utama dengan metode yang sound
Bahkan program dalam bahasa yang jauh dari Turing-complete—tanpa heap, tanpa pointer, tanpa integer, hanya variabel Boolean, dan loop yang tidak bisa berulang lebih dari dua kali—juga tidak dapat diverifikasi secara praktis karena dapat direduksi ke TQBF. Untuk properti tertentu, misalnya keamanan memori, hal itu mungkin dilakukan, tetapi itu belum cukup untuk kebutuhan perangkat lunak. Pada 1970–1990-an ada harapan bahwa meski kompleksitas kasus terburuk sulit ditangani, jaminan lokal dan struktur bahasa akan membantu menghindari kasus terburuk; namun kemudian terbukti tidak demikian. Harapan bahwa program yang benar-benar ditulis manusia cukup jauh dari kasus terburuk sehingga akan muncul heuristik yang baik juga tampaknya kini tidak berlaku
Ada presentasi yang membahas hal terkait: https://pron.github.io/posts/correctness-and-complexity
Hasil intinya adalah sebagian besar properti menarik yang ingin diverifikasi tidak bersifat komposisional. Sekalipun kita membuktikan properti untuk masing-masing komponen P1...Pn, biaya membuktikan properti itu untuk P1 ○ ... ○ Pn tidak hanya tumbuh superpolinomial terhadap n, tetapi juga superpolinomial terhadap ukuran tiap komponen. Artinya, tingkat kesulitannya sama seperti ketika tidak dipecah, dan kebenaran tidak dapat didekomposisi. Jadi “cukup banyak hal yang bisa diverifikasi” dan “yang bisa diverifikasi hanyalah setetes air di lautan” sama-sama benar, dan dalam diskusi teknik formal, jurang di antara keduanya sering terlewat
Selama lebih dari 6 tahun terakhir, saya telah mengulang argumen yang sama ratusan kali di HN, dan meski sudah menerima banyak komentar selama itu, hampir tidak ada nuansa yang ditambahkan
Itu tidak sepenuhnya salah, tetapi juga tidak sepenuhnya benar. Banyak orang yang tertarik pada topik ini punya banyak kesempatan, melalui ratusan pengulangan, untuk menunjukkan hal tersebut, jadi mengejutkan bahwa posisi itu sama sekali tidak berkembang. Sikap seperti ini terdengar seperti ketertutupan yang patologis, dan membuat semua orang yang ikut berdiskusi membuang waktu
Saya melihat fokus pada soundness justru mengalihkan perhatian dari teknik-teknik yang terbukti lebih berhasil dalam mencapai tujuan perangkat lunak yang lebih benar. Ada teknik praktis yang juga didukung secara teoretis, dan kadang mengejutkan orang-orang yang mengira soundness adalah satu-satunya jalan: http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h...
Hal seperti ini terus berulang. Sementara metode sound mendapatkan perbaikan penting, metode yang tidak sound justru membuat kemajuan yang jauh lebih besar dalam praktik menuju perangkat lunak yang lebih benar. Contoh yang sangat baru adalah https://antithesis.com. Tentu saja, dalam situasi tertentu teknik yang sound bisa lebih kuat dan praktis, jadi ini topik yang kompleks
Masuk akal untuk berharap bahwa library Rust kecil dapat diverifikasi apakah menggunakan unsafe dengan benar. Itu saja sudah benar-benar berguna
Saya juga baru saja menulis komentar terkait pada tulisan F*. Dari sisi sintaks saja, secara subjektif saya lebih menyukai F*/F# daripada Rust, tetapi untuk perangkat lunak kontrol pertunjukan yang sedang saya kembangkan, saya memutuskan memakai Ada/SPARK2014
Agar Rust dapat menarik orang-orang yang sama seperti Ada/SPARK2014, Rust memerlukan standar resmi yang diterbitkan seperti bahasa-bahasa lama semacam C, Common Lisp, Prolog, Fortran, dan COBOL. AdaCore dan Ferrous Systems sedang bekerja sama untuk menyediakan alat verifikasi formal bagi Rust seperti Ada/SPARK2014, sehingga Rust juga mulai masuk ke ranah ini, tetapi belum ada standar yang diterbitkan, dan warisan Ada serta SPARK2014 sangat besar
Menarik bahwa reference counting dapat dipandang sebagai semacam GC teroptimasi yang berjalan langsung, yang bekerja saat digunakan untuk data yang benar-benar asiklik atau ketika kebocoran siklik bisa diterima. Python menggunakan pendekatan campuran reference counting + tracing seperti yang dijelaskan dalam tulisan itu, dan saya juga pernah melihat deployment operasional yang memaksa collector tracing hanya berjalan sekali setiap N request
Perl memakai reference counting murni, tetapi memiliki weak reference, sehingga dengan konsekuensi harus memperhatikan bagian mana dari struktur siklik yang referensinya dipertahankan, data bisa dibuat asiklik dari sudut pandang reference counting. Koka secara teori memakai reference counting, tetapi dalam praktiknya berusaha memindahkannya sebanyak mungkin ke waktu kompilasi; jika pada y = x + 1 dijamin bahwa x hanya memiliki satu referensi dan tidak dipakai lagi setelahnya, penyimpanan yang sama dapat dipakai ulang untuk y sehingga bisa diubah in-place
Nim menyediakan ORC, yaitu automatic reference counting yang ditambah implementasi algoritma Recycler dari Bacon+Rajan. Algoritma ini dirancang untuk mengumpulkan hanya siklus dalam sistem berbasis reference counting, sehingga cukup cepat. Kembali ke Rust, implementasi Recycler stop-the-world ada di sini: https://github.com/fitzgen/bacon-rajan-cc dan fork ini didistribusikan sebagai crate bacon-rajan-ccc: https://github.com/mbartlett21/bacon-rajan-cc Bagian Alternative di README menautkan eksperimen lain di ranah yang sama. Jika sulit menemukan makalah Recycler, salinannya dikumpulkan di bawah https://trout.me.uk/gc/, dan jika selera Anda serupa, makalah-makalah di bawah https://trout.me.uk/lisp/ juga mungkin akan Anda nikmati
Firefox juga menggunakan reference counting bersama cycle collector berbasis trial deletion untuk mengelola siklus melalui objek DOM C++ dan JS. Bahkan Graydon-lah yang menangani implementasi awalnya
Saya merasa tidak sabar terhadap verifikasi formal program. Pembuktian bahwa sebuah program mengimplementasikan spesifikasi dengan benar memang menarik secara teori, tetapi kegunaan praktisnya kecil
Menulis spesifikasi yang benar sama sulitnya dengan pemrograman yang benar, jadi masalah yang sulit tidak benar-benar terselesaikan, hanya dipindahkan. Teknik formal punya penggunaan praktis, tetapi jarang ditemui
Benar jika yang dimaksud adalah spesifikasi lengkap, tetapi itu bukan tujuan sebenarnya. Biasanya yang ingin dibuktikan adalah beberapa properti inti. Misalnya, fungsi ini selalu berhenti, atau fungsi itu selalu mengembalikan array yang sudah terurut
Begitu hal seperti itu bisa dilakukan, ia dapat dipaksakan sebagai prasyarat. Misalnya, sebelum meneruskan array ke suatu fungsi, Anda harus menunjukkan bahwa array tersebut sudah diurutkan sebelumnya
Ditulis pada 15 Mei 2024, dan hari itu adalah ulang tahun ke-9 Rust 1.0
Saya membaca tulisan Boats yang ditautkan dan itu luar biasa. Saya terkejut bahwa kutipan Hoare dari 50 tahun lalu masih relevan dan ungkapannya juga sangat bagus
Akan menyenangkan jika kita bisa memakai sesuatu seperti type guard waktu kompilasi dengan cara yang lebih sederhana. Ketika trait bound menjamur, program level tipe menjadi sulit dibaca
Misalnya seperti Where <<::Output as G>::Output as H>::Output: HList + Z atau type Output = <<::Output as G>::Output as H>::Output;. Lalu Anda memasukkan Cons>>> ke sana, dan menyadari bahwa angka seperti U8 dari TypeNum pun pada dasarnya adalah nesting Cons>> juga. Di ranah ini, memang mungkin membuat kemajuan dan melakukan verifikasi yang diinginkan, tetapi pesan error bisa sangat berbeda dari cara developer manusia menulis kode, dan implementasinya juga sangat menyakitkan
Alasan developer experience-nya mengejutkan adalah karena ini bukan “sekadar fungsi”, melainkan kombinasi spesifik antara generic dan associated type. Saya ingin memakai pemeriksaan bergaya runtime tetapi menjalankannya pada waktu kompilasi, namun untuk melakukannya saya harus menulis kode yang cukup berbeda. Pada akhirnya, membuat Rust waktu kompilasi level tipe menjadi lebih sederhana, fungsional, dan mudah dibaca mungkin adalah jalan agar proyek analisis formal seperti ini memberikan pengalaman yang baik bagi maintainer dan pengguna. Singkatnya, saya menginginkan Rust comptime. Dan saya juga penasaran apakah Future berbasis Pin<&mut Self> sudah terlanjur mapan. Saya ingin bereksperimen dengan implementasi internal lain untuk async/await, tetapi tidak tahu harus mulai dari mana
1 komentar
Komentar Hacker News
Tulisan yang bagus. Dari sudut pandang seseorang yang dulu pernah melakukan verifikasi program, Rust tampak seperti bahasa modern yang paling berguna untuk menerapkan teknik formal
Aturan Rust menghilangkan banyak kasus yang sulit diformalkan. Masalah besar yang tersisa adalah analisis deadlock dari perspektif thread dan perspektif
Rc/borrow, dan keduanya sampai batas tertentu setara. Jika Rust memiliki analisis deadlock statis, tampaknya pointer dereference yang aman juga bisa dimungkinkan, dan jika dapat dibuktikan bahwa semua pemanggilan borrow/upgrade tidak gagal, sebagian besar reference count bisa dihapus. Dengan begitu, jika memungkinkan, mutabilitas internal juga bisa didapatkan secara gratisMasalah besar theorem prover adalah karena dibuat oleh orang-orang yang suka membuktikan teorema, mereka cenderung terjebak dalam formalisme sehingga rasa UI dan programmer-nya melenceng. Sebagian besar kewajiban pembuktian dapat ditangani dengan SAT solver, tetapi masalah yang sulit membutuhkan alat yang lebih berat. Coq terlalu manual, dan penulis menganggap ACL2 terlalu fungsional. Machine learning bisa membantu mengarahkan theorem prover. Sulit menyerahkan pembuktian itu sendiri, tetapi tampaknya mungkin untuk menyimpulkan rencana pembuktian pada kode yang alur kontrol dan penggunaan datanya umumnya mirip
Rutin kriptografi Firefox dan Wireguard ditulis bukan dalam Rust, melainkan F*, lebih tepatnya Low*, DSL tingkat rendah yang tertanam di F*, dan telah diverifikasi sepenuhnya
https://project-everest.github.io/
https://mitls.org/
Masalah saat menerapkan alat seperti ini untuk memverifikasi bahasa eksternal seperti Rust adalah pembuktian tidak ditulis dalam bahasa target, sehingga developer harus mempelajari dua bahasa. Berdasarkan pengalaman menulis Creusot, pekerjaan pada Verus dan Aeneas, serta pengalaman di laboratorium Why3, saya telah memikirkan seperti apa “Rust yang sadar verifikasi” itu. Jika bahasa seperti itu dibuat dari awal, kemudahan verifikasinya bisa meningkat secara bertahap bahkan dibanding Rust, dan tampaknya akan sangat efektif terutama pada bagian pembuktian yang sulit
Fitur bawaan yang paling saya rasa kurang adalah sesuatu seperti “jalankan quickcheck pada bukti saya”. Ketika ada kode dan kita mencoba membuktikan properti yang ternyata tidak benar, mudah sekali pusing memikirkan kenapa buktinya tidak jalan. Saat di tengah pembuktian kita mencapai keadaan yang tidak masuk akal, akan menyenangkan jika ada perintah seperti “coba buat counterexample di sini” yang mengeluarkan counterexample. Pembuktian sangat bergantung pada jalur dan umumnya tidak mudah, tetapi alat-alat ini tampak sangat dekat dengan kehebatan. Proses mencoba membuktikan kode juga harus mencerminkan kemungkinan bahwa kode itu bisa memiliki bug
Prover tidak menghasilkan bukti yang salah, ia hanya gagal menghasilkan bukti yang valid. Menurut saya tidak banyak penerapan machine learning yang memiliki sifat seperti ini
Sebenarnya di Rust, lock dan reference count adalah struktur runtime.
Arcsangat merusak model RAII Rust, sehingga scoped thread yang destruktornya harus berjalan sebelum scope berakhir harus dihapus. Reference count global punya masalah siklus dan kebocoran, dan kembali menjadi masalah global. Mungkin sulit menghilangkannya sepenuhnya, tetapi saya percaya lebih baik mengurungnya dalam scope bergaya arena. Untuk lock, tampaknya diperlukan struktur data asimetris seperti channel. Di Go, channel dibagi menjadi sender dan receiver, dan di goroutine pengirim kita bisa memasangdefer close(ch), yang dijamin dieksekusi setelah sisa thread selesai bahkan jika terjadi panic. Tidak harus channel, tetapi memisahkan peran baca-tulis/produsen-konsumen akan membuat penalaran jauh lebih mudah dan tampaknya juga membantu analisis formalSaya suka bagaimana ini dimulai dari kutipan makalah Hoare sekitar 1973 dan kini berlanjut sampai tulisan kedua. Awalnya saya menulis komentar panjang di thread HN untuk tulisan boat, mengatakan bahwa memiringkan kutipan itu ke sudut pandang yang berpusat pada Rust bisa dimengerti mengingat latar belakang boat, tetapi itu mempersempit cakupan kritik Hoare secara artifisial
Sekarang Grayson menjadikan potongan sempit itu sebagai titik awal untuk membahas beberapa wilayah dan titik desain Rust yang menarik. Saya masih merasa komentar saya benar, tetapi diskusi yang berlanjut dari tulisan Grayson sudah cukup untuk menutupi keberatan teknis saya terhadap tulisan yang menjadi titik awalnya
Setelah itu, dengan munculnya teknik-teknik unsound yang lebih maju daripada sekadar pengujian sederhana, menurut saya metode unsound justru melangkah lebih jauh daripada metode sound
Ia menemukan masalahnya, dan jika dilihat ke belakang, solusi memaksakan sharing XOR mutability melalui sistem tipe tampak seperti satu langkah kecil. Seandainya saat itu orang menyadari bahwa langkah kecil itulah solusinya, penderitaan luar biasa selama 50 tahun bisa berkurang
Namun saya tidak melihat kutipan itu sendiri memperkuat sudut pandang tersebut. Bisa dilihat sebagai upaya mengambil keluhan Hoare yang lebih umum tentang keberadaan semantik referensi itu sendiri, lalu menerapkannya pada model state mutable tanpa alias milik Rust untuk menghindari masalah. Namun ini lebih mirip memperbaiki hanya potongan sempit dari masalah yang lebih besar lalu mengatakan seluruh masalahnya sudah hilang. Bagian-bagian yang hilang, khususnya awal bagian “Variables” dan contoh ALGOL 68, jauh lebih kuat mengarah pada bahwa Hoare mengkritik konsep semantik referensi itu sendiri, bukan sekadar state mutable. Saya mengakui Rust adalah upaya untuk menjinakkan sebagian masalah, tetapi saya tidak melihat ada bahasa mana pun yang telah “memperbaiki” masalah ini
Saya tidak begitu mengerti mengapa tulisan ini mendapat begitu banyak pujian. Rasanya seperti menyapu berbagai bidang analisis program dalam satu paragraf. Saya menyukai Graydon dan menghormati sudut pandangnya, tetapi paragraf ini terlalu menyederhanakan
Penjelasan seolah-olah bahasa dengan GC sengaja tidak memiliki dukungan kuat untuk penalaran lokal adalah strawman. Ada bahasa seperti Pony yang memakai GC sambil tetap menempatkan region di sistem tipenya. Selain itu ada seluruh bidang analisis pointer dan analisis escape, yang menginfer keunikan dan menentukan apakah dua referensi mungkin menjadi alias. Inti dari tipe statis juga adalah membagi heap menjadi bagian-bagian yang tidak saling ber-alias melalui teknik seperti class dan field. Ini bukan soal JavaScript, dan kita tidak boleh berpura-pura bahwa Java/C#/Scala serta banyak bahasa GC tidak memiliki penalaran lokal atas state mutable
Class dan field tidak menyediakan penalaran lokal penuh atas state mutable. Sebab class/objek A bisa saja bergantung pada state mutable class/objek B. Pewarisan class ala Java dengan sendirinya menambahkan lebih banyak kompleksitas seiring program berevolusi dari waktu ke waktu
Tentu ada contoh tandingan, tetapi jika melihat bahasa GC serbaguna arus utama seperti Java, C#, dan Python, pernyataan itu benar. Bisa ditafsirkan bahwa gagasan awal object-oriented lebih dekat dengan actor model saat ini, dan dimaksudkan untuk mengubah struktur data yang dimiliki hanya lewat pengiriman pesan. Namun implementasi object-oriented di dunia nyata hampir tidak mendekati tujuan itu. Java tidak mencegah penyimpanan referensi mutable ke objek yang sama di banyak objek. Tulisan ini menjelaskan poin itu dengan lebih baik: https://without.boats/blog/references-are-like-jumps/
void myMethod(final Map map) { map.remove("key"); int oldSize = map.size(); map.put("key", "val"); int newSize = map.size(); System.out.println(newSize - oldSize); }Edit: saya salah membaca negasi ganda. Bahkan setelah dibaca ulang, tetap membingungkan. Maksudnya Java memiliki penalaran lokal, tidak seperti JavaScript?
Biasanya saya menyukai tulisan Graydon, tetapi tulisan ini, seperti banyak tulisan tentang teknik formal, bisa menyesatkan pembaca yang tidak mengenal bidangnya. Ini mirip dengan mengatakan bahwa cara mengubah timbal menjadi emas sudah meningkat beberapa orde satu digit, tetapi tidak mengatakan bahwa masih tersisa 29 orde lagi sebelum efisiensi biaya praktis tercapai
Apakah tidak adanya alias sangat memudahkan verifikasi formal? Ya. Tetapi apakah itu berarti program dunia nyata dapat diverifikasi secara praktis dan hemat biaya? Sama sekali tidak. Ada program, sirkuit, dan komponen yang diverifikasi secara formal setiap hari, tetapi itu lebih merupakan pengecualian, relatif sangat kecil, dan dibuat dengan cara yang sangat hati-hati. Properti yang membantu penalaran lokal memang penting, tetapi tidak memberi perubahan nyata pada cara menjamin kebenaran perangkat lunak arus utama dengan metode yang sound
Bahkan program dalam bahasa yang jauh dari Turing-complete—tanpa heap, tanpa pointer, tanpa integer, hanya variabel Boolean, dan loop yang tidak bisa berulang lebih dari dua kali—juga tidak dapat diverifikasi secara praktis karena dapat direduksi ke TQBF. Untuk properti tertentu, misalnya keamanan memori, hal itu mungkin dilakukan, tetapi itu belum cukup untuk kebutuhan perangkat lunak. Pada 1970–1990-an ada harapan bahwa meski kompleksitas kasus terburuk sulit ditangani, jaminan lokal dan struktur bahasa akan membantu menghindari kasus terburuk; namun kemudian terbukti tidak demikian. Harapan bahwa program yang benar-benar ditulis manusia cukup jauh dari kasus terburuk sehingga akan muncul heuristik yang baik juga tampaknya kini tidak berlaku
Ada presentasi yang membahas hal terkait: https://pron.github.io/posts/correctness-and-complexity
Hasil intinya adalah sebagian besar properti menarik yang ingin diverifikasi tidak bersifat komposisional. Sekalipun kita membuktikan properti untuk masing-masing komponen P1...Pn, biaya membuktikan properti itu untuk P1 ○ ... ○ Pn tidak hanya tumbuh superpolinomial terhadap n, tetapi juga superpolinomial terhadap ukuran tiap komponen. Artinya, tingkat kesulitannya sama seperti ketika tidak dipecah, dan kebenaran tidak dapat didekomposisi. Jadi “cukup banyak hal yang bisa diverifikasi” dan “yang bisa diverifikasi hanyalah setetes air di lautan” sama-sama benar, dan dalam diskusi teknik formal, jurang di antara keduanya sering terlewat
Itu tidak sepenuhnya salah, tetapi juga tidak sepenuhnya benar. Banyak orang yang tertarik pada topik ini punya banyak kesempatan, melalui ratusan pengulangan, untuk menunjukkan hal tersebut, jadi mengejutkan bahwa posisi itu sama sekali tidak berkembang. Sikap seperti ini terdengar seperti ketertutupan yang patologis, dan membuat semua orang yang ikut berdiskusi membuang waktu
Hal seperti ini terus berulang. Sementara metode sound mendapatkan perbaikan penting, metode yang tidak sound justru membuat kemajuan yang jauh lebih besar dalam praktik menuju perangkat lunak yang lebih benar. Contoh yang sangat baru adalah https://antithesis.com. Tentu saja, dalam situasi tertentu teknik yang sound bisa lebih kuat dan praktis, jadi ini topik yang kompleks
unsafedengan benar. Itu saja sudah benar-benar bergunaSaya juga baru saja menulis komentar terkait pada tulisan F*. Dari sisi sintaks saja, secara subjektif saya lebih menyukai F*/F# daripada Rust, tetapi untuk perangkat lunak kontrol pertunjukan yang sedang saya kembangkan, saya memutuskan memakai Ada/SPARK2014
Agar Rust dapat menarik orang-orang yang sama seperti Ada/SPARK2014, Rust memerlukan standar resmi yang diterbitkan seperti bahasa-bahasa lama semacam C, Common Lisp, Prolog, Fortran, dan COBOL. AdaCore dan Ferrous Systems sedang bekerja sama untuk menyediakan alat verifikasi formal bagi Rust seperti Ada/SPARK2014, sehingga Rust juga mulai masuk ke ranah ini, tetapi belum ada standar yang diterbitkan, dan warisan Ada serta SPARK2014 sangat besar
Menarik bahwa reference counting dapat dipandang sebagai semacam GC teroptimasi yang berjalan langsung, yang bekerja saat digunakan untuk data yang benar-benar asiklik atau ketika kebocoran siklik bisa diterima. Python menggunakan pendekatan campuran reference counting + tracing seperti yang dijelaskan dalam tulisan itu, dan saya juga pernah melihat deployment operasional yang memaksa collector tracing hanya berjalan sekali setiap N request
Perl memakai reference counting murni, tetapi memiliki weak reference, sehingga dengan konsekuensi harus memperhatikan bagian mana dari struktur siklik yang referensinya dipertahankan, data bisa dibuat asiklik dari sudut pandang reference counting. Koka secara teori memakai reference counting, tetapi dalam praktiknya berusaha memindahkannya sebanyak mungkin ke waktu kompilasi; jika pada
y = x + 1dijamin bahwaxhanya memiliki satu referensi dan tidak dipakai lagi setelahnya, penyimpanan yang sama dapat dipakai ulang untukysehingga bisa diubah in-placeNim menyediakan ORC, yaitu automatic reference counting yang ditambah implementasi algoritma Recycler dari Bacon+Rajan. Algoritma ini dirancang untuk mengumpulkan hanya siklus dalam sistem berbasis reference counting, sehingga cukup cepat. Kembali ke Rust, implementasi Recycler stop-the-world ada di sini: https://github.com/fitzgen/bacon-rajan-cc dan fork ini didistribusikan sebagai crate bacon-rajan-ccc: https://github.com/mbartlett21/bacon-rajan-cc Bagian Alternative di README menautkan eksperimen lain di ranah yang sama. Jika sulit menemukan makalah Recycler, salinannya dikumpulkan di bawah https://trout.me.uk/gc/, dan jika selera Anda serupa, makalah-makalah di bawah https://trout.me.uk/lisp/ juga mungkin akan Anda nikmati
Saya merasa tidak sabar terhadap verifikasi formal program. Pembuktian bahwa sebuah program mengimplementasikan spesifikasi dengan benar memang menarik secara teori, tetapi kegunaan praktisnya kecil
Menulis spesifikasi yang benar sama sulitnya dengan pemrograman yang benar, jadi masalah yang sulit tidak benar-benar terselesaikan, hanya dipindahkan. Teknik formal punya penggunaan praktis, tetapi jarang ditemui
Begitu hal seperti itu bisa dilakukan, ia dapat dipaksakan sebagai prasyarat. Misalnya, sebelum meneruskan array ke suatu fungsi, Anda harus menunjukkan bahwa array tersebut sudah diurutkan sebelumnya
Ditulis pada 15 Mei 2024, dan hari itu adalah ulang tahun ke-9 Rust 1.0
Saya membaca tulisan Boats yang ditautkan dan itu luar biasa. Saya terkejut bahwa kutipan Hoare dari 50 tahun lalu masih relevan dan ungkapannya juga sangat bagus
Akan menyenangkan jika kita bisa memakai sesuatu seperti type guard waktu kompilasi dengan cara yang lebih sederhana. Ketika trait bound menjamur, program level tipe menjadi sulit dibaca
Misalnya seperti
Where <<::Output as G>::Output as H>::Output: HList + Zatautype Output = <<::Output as G>::Output as H>::Output;. Lalu Anda memasukkanCons>>>ke sana, dan menyadari bahwa angka sepertiU8dari TypeNum pun pada dasarnya adalah nestingCons>>juga. Di ranah ini, memang mungkin membuat kemajuan dan melakukan verifikasi yang diinginkan, tetapi pesan error bisa sangat berbeda dari cara developer manusia menulis kode, dan implementasinya juga sangat menyakitkanAlasan developer experience-nya mengejutkan adalah karena ini bukan “sekadar fungsi”, melainkan kombinasi spesifik antara generic dan associated type. Saya ingin memakai pemeriksaan bergaya runtime tetapi menjalankannya pada waktu kompilasi, namun untuk melakukannya saya harus menulis kode yang cukup berbeda. Pada akhirnya, membuat Rust waktu kompilasi level tipe menjadi lebih sederhana, fungsional, dan mudah dibaca mungkin adalah jalan agar proyek analisis formal seperti ini memberikan pengalaman yang baik bagi maintainer dan pengguna. Singkatnya, saya menginginkan Rust
comptime. Dan saya juga penasaran apakahFutureberbasisPin<&mut Self>sudah terlanjur mapan. Saya ingin bereksperimen dengan implementasi internal lain untukasync/await, tetapi tidak tahu harus mulai dari mana