Apa yang dilakukan oleh perancang bahasa untuk memutuskan atau membuktikan bahwa fitur tertentu berfungsi dengan benar?

Saya tertarik pada desain bahasa dan secara umum saya dapat dengan mudah menjelaskan tentang fitur-fitur yang dikenal luas (misalnya warisan, polimorfisme, delegasi, lambda, tangkapan, pengumpulan sampah, pengecualian, generik, varian, refleksi, dan sebagainya), interaksi mereka dalam bahasa tertentu, cara-cara mereka dapat diimplementasikan, keterbatasan mereka, dll.

Dalam beberapa bulan terakhir, saya mulai membaca tentang Rust, yang memiliki sistem kepemilikan yang menjamin keamanan memori dan manajemen sumber daya deterministik dengan memaksa masa hidup objek untuk diverifikasi secara statis. Dari sudut pandang pengguna bahasa yang sederhana, saya bisa segera mengambil sistem.

Namun, dari sudut pandang perancang bahasa, saya perlu waktu untuk menyadari mengapa segala sesuatu di Rust persis seperti itu. Saya tidak dapat segera memahami alasan di balik beberapa pembatasan sistem kepemilikan, sampai saya memaksakan diri untuk mengajukan kasus yang akan melanggar integritas sistem jika tidak memiliki aspek-aspek tersebut.

Pertanyaan utama saya tidak ada hubungannya dengan Rust dan kepemilikannya secara khusus - tetapi jangan ragu untuk menggunakannya sebagai contoh dalam komentar / jawaban Anda, jika perlu.

Ketika perancang bahasa merancang fitur baru, metodologi atau proses apa yang mereka gunakan untuk memutuskan bahwa fitur tersebut berfungsi dengan baik?

Maksud "baru" yang saya maksudkan bukanlah sesuatu yang telah diuji dalam bahasa yang ada (dan dengan demikian sebagian besar pekerjaan telah dilakukan oleh desainer lain). Dengan "berfungsi sebagaimana mestinya" maksud saya bahwa fitur memecahkan masalah yang dimaksud dengan benar, dan itu cukup antipeluru. Dengan "cukup antipeluru" Maksud saya tidak ada kode yang dapat ditulis dalam bahasa atau bagian tertentu dari bahasa (misalnya subset tanpa kode "tidak aman") yang akan melanggar integritas fitur.

• Apakah ini proses coba-coba, dalam artian Anda menemukan bentuk fitur yang sederhana, kemudian mencoba menemukan cara untuk melanggarnya, kemudian menambalnya jika Anda berhasil melanggarnya, kemudian ulangi? Dan kemudian, ketika Anda tidak bisa memikirkan kemungkinan pelanggaran lain, Anda berharap tidak ada yang tersisa dan menyebutnya sehari?

• Atau adakah cara formal untuk benar-benar membuktikan (dalam pengertian matematika dari kata) bahwa fitur Anda berfungsi dan kemudian menggunakan bukti itu untuk dengan percaya diri mendapatkan fitur yang benar (atau sebagian besar benar) sejak awal?

(Saya harus menyebutkan bahwa saya memiliki latar belakang teknik, bukan ilmu komputer. Jadi jika saya kehilangan sesuatu yang jelas bagi orang-orang CS, jangan ragu untuk menunjukkannya.)

Saya mengalami kesulitan menemukan referensi yang tepat saat ini, tetapi beberapa saat yang lalu saya menonton beberapa video oleh Simon Peyton Jones , yang merupakan kontributor utama untuk desain Haskell. Dia adalah pembicara yang sangat baik tentang teori jenis, desain bahasa, dan sejenisnya, omong-omong, dan memiliki banyak video yang tersedia secara gratis di youtube.

Haskell memiliki representasi perantara yang pada dasarnya lambda calculus ditambah dengan beberapa hal sederhana untuk membuatnya lebih mudah untuk dikerjakan. Kalkulus Lambda telah digunakan dan terbukti sejak komputer hanyalah orang yang menghitung sesuatu. Hal yang menarik yang sering dibuat Simon Peyton Jones adalah bahwa setiap kali mereka melakukan sesuatu yang liar dan gila dengan bahasa tersebut, ia tahu itu pada dasarnya terdengar ketika akhirnya berkurang kembali ke bahasa perantara itu.

Bahasa lain hampir tidak begitu ketat, tetapi lebih memilih kemudahan penggunaan atau implementasi. Mereka melakukan hal yang sama seperti yang dilakukan oleh programmer lain untuk mendapatkan kode berkualitas tinggi: mengikuti praktik pengkodean yang baik dan mengujinya sampai mati. Sebuah fitur seperti semantik kepemilikan Rust, saya yakin mendapatkan banyak analisis formal dan pengujian untuk menemukan kasus sudut yang terlupakan. Seringkali fitur seperti itu dimulai sebagai tesis pascasarjana seseorang.

Jadi untuk desain bahasa , ada bukti (atau bug). Misalnya, ketik sistem. Jenis dan Bahasa Pemrograman adalah buku kanonik yang menggambarkan sistem tipe, dan berfokus pada pembuktian kebenaran dan kelengkapan sistem tipe. Tata bahasa memiliki analisis yang serupa, dan algoritma (seperti sistem kepemilikan yang Anda gambarkan) memiliki analisis sendiri.

Untuk implementasi bahasa , ini adalah kode seperti yang lain. Anda menulis tes unit. Anda menulis tes integrasi. Anda melakukan review kode.

Satu-satunya hal yang membuat bahasa istimewa adalah bahwa mereka (hampir selalu) tidak terbatas. Anda benar-benar tidak dapat menguji semua input. Dan (idealnya) mereka digunakan oleh banyak orang, melakukan hal-hal aneh dan menarik, sehingga bug apa pun dalam bahasa tersebut akan ditemukan pada akhirnya.

Secara praktis , relatif sedikit bahasa menggunakan bukti untuk memverifikasi fungsinya, dan berakhir dengan beberapa campuran opsi yang Anda sebutkan.

Hal pertama dan paling sulit yang harus diperhatikan oleh perancang bahasa saat memperkenalkan fitur baru, adalah menjaga konsistensi bahasanya:

• bagaimana itu dapat diintegrasikan dalam tata bahasa tanpa melanggar kode yang ada (ini dapat dibuktikan secara matematis)
• bagaimana hubungannya dengan fitur yang ada (misalnya jika Anda telah memperbaiki array yang diindeks 0..n-1, Anda tidak akan memperkenalkan fitur array variabel baru yang diindeks 1..n) (itulah bagian artistik dari desain)
• bagaimana fitur dapat diimplementasikan di seluruh rantai alat sehingga fitur baru dapat diserap oleh ekosistem, pembuat alat dan programmer (kelayakan dapat ditunjukkan dengan bukti konsep, tetapi implementasi penuh adalah pendekatan yang mirip dengan pemrograman)

Untuk memandu dalam hal ini, seorang desainer bergantung pada seperangkat aturan dan prinsip desain. Pendekatan ini dijelaskan dengan sangat baik dalam " Desain dan evolusi C ++ " dari Bjarne Stroustrup , salah satu buku langka yang didedikasikan untuk desain bahasa. Yang sangat menarik adalah melihat bahwa bahasa jarang dirancang dalam ruang hampa, dan perancang juga melihat bagaimana bahasa mereka telah menerapkan fitur serupa. Sumber lain (online dan gratis) adalah prinsip-prinsip desain untuk bahasa java .

Jika Anda melihat proses publik komite standardisasi, Anda akan melihat bahwa itu lebih merupakan proses kesalahan uji coba. Berikut ini contoh pada modul C ++ konsep yang sepenuhnya baru untuk diperkenalkan dalam versi bahasa berikutnya. Dan di sini analisis disusun setelah beberapa perubahan bahasa , untuk menilai keberhasilannya. Dan di sini Java Community Process untuk mendefinisikan spesifikasi Java baru, seperti api baru . Anda akan melihat bahwa pekerjaan ini dilakukan oleh beberapa ahli yang membuat konsep makalah konsep dan proposal pertama secara kreatif. Kemudian proposal ini ditinjau oleh komunitas / komite yang lebih besar yang dapat mengubah proposal untuk memastikan tingkat konsistensi yang lebih tinggi.

Bagaimana cara menguji fitur bahasa pemrograman? Ini adalah pertanyaan yang sangat bagus, dan saya tidak yakin bahwa keadaan seni sampai pada pekerjaan.

Setiap fitur baru dapat berinteraksi dengan semua fitur lainnya. (Ini memengaruhi bahasa, dokumen, kompiler, pesan kesalahan, IDE, pustaka, dll.) Apakah fitur digabungkan untuk membuka celah? Untuk membuat kasus tepi yang buruk?

Bahkan perancang bahasa yang sangat cerdas yang bekerja keras untuk menjaga kesehatan tipe menemukan pelanggaran seperti bug Rust ini . Sistem tipe Rust tidak begitu jelas bagi saya, tetapi saya pikir dalam kasus ini memiliki sistem nilai track type seumur hidup berarti "subtyping" seumur hidup bentrok dengan harapan untuk subtyping biasa, paksaan, referensi, dan mutabilitas, menciptakan celah di mana staticseumur hidup ref dapat menunjuk ke nilai yang dialokasikan stack dan kemudian menjadi referensi yang menggantung.

Dengan "berfungsi sebagaimana mestinya" maksud saya bahwa fitur memecahkan masalah yang dimaksud dengan benar, dan itu cukup antipeluru.

Untuk bahasa yang dimaksudkan sebagai bahasa produksi , yaitu, yang digunakan oleh banyak programmer untuk membangun perangkat lunak produksi yang andal, "berfungsi dengan baik" harus lebih jauh berarti menyelesaikan masalah yang dimaksud dengan benar untuk audiens yang dituju.

Dengan kata lain, kegunaan sama pentingnya dengan desain bahasa seperti halnya untuk jenis desain lainnya. Ini mensyaratkan (1) desain untuk kegunaan (misalnya mengetahui audiens Anda), dan (2) pengujian kegunaan.

Contoh artikel tentang topik ini adalah " Programmer adalah Orang, Juga , Bahasa pemrograman dan desainer API dapat belajar banyak dari bidang desain faktor manusia."

Contoh pertanyaan SE tentang topik ini adalah apakah sintaksis bahasa pemrograman apa pun telah diuji kegunaannya?

Contoh uji usability dianggap memperluas fitur iterasi daftar (saya tidak ingat bahasa mana) untuk mengambil beberapa daftar. Apakah orang berharap untuk beralih melalui daftar secara paralel atau melalui produk-silang? Perancang bahasa terkejut dengan temuan tes kegunaan.

Bahasa seperti Smalltalk, Python, dan Dart dirancang dengan penekanan pada kegunaan. Jelas Haskell tidak.