Apa "pertanyaan" yang coba dijawab oleh teori bahasa pemrograman?

Saya telah tertarik pada berbagai topik seperti Combinatory Logic, Lambda Calculus, Functional Programming untuk sementara waktu dan telah mempelajarinya. Namun, tidak seperti "Theory of Computation" yang berusaha menjawab pertanyaan "computability" yaitu, hal-hal yang dapat / tidak dapat dihitung dengan berbagai kendala, saya berjuang untuk menemukan analog untuk "Theory of Programming"

Wikipedia menggambarkannya sebagai:

Teori bahasa pemrograman (PLT) adalah cabang ilmu komputer yang berhubungan dengan desain, implementasi, analisis, karakterisasi, dan klasifikasi bahasa pemrograman dan fitur-fitur individualnya.

Ini seperti mengatakan "segalanya" yang tidak terlalu spesifik.

Kemajuan umum dari topik biasanya seperti:

Logika Combinatory> Lambda Calculus> Martin Lof Type Theory> Typed Lambda Calculus> (Sesuatu terjadi di sini)> Bahasa pemrograman berkembang - yang hanya memiliki sedikit koneksi dengan CL / $\lambda$

$\lambda$

$\lambda$

Tujuan keseluruhan PLT adalah membuat rekayasa perangkat lunak industri (dalam arti umum) lebih murah (juga dalam arti umum), melalui mengoptimalkan alat yang paling penting (bahasa pemrograman) dan ekosistem perkakas terkait.

Beberapa alasan mengapa matematika terlibat:

• PL sangat tidak sepele, dan tidak jelas bahwa mereka melakukan hal yang benar tanpa bukti. Matematika memberikan model bahasa pemrograman yang disederhanakan . Model ini memungkinkan kita mempelajari bahasa pemrograman nyata dalam pengaturan yang jauh lebih sederhana, menghapus (semoga) sebagian besar masalah sudah di tingkat model. Bahasa pemrograman nyata saat ini sulit secara matematis. Dengan kata lain: lambda-calculus adalah lalat buah, E.Coli, sapi bulat PLT.

• PLT tidak memiliki metode empiris yang cocok, yang akan menyenangkan / lebih baik untuk dimiliki, sehingga matematika dilakukan sebagai pengganti.

• Matematika itu indah dan mendalam.

• Matematika memberikan metodologi penelitian yang sederhana, dicoba dan diuji, yang penting untuk membantu lulusan PhD seseorang. Biasanya, beberapa varian misalnya: Selidiki fitur PL XYZ dengan menambahkannya ke lambda-calculus. Tambahkan tipe sederhana untuk XYZ dan buktikan tipe-kesehatan. Tambahkan obat generik untuk XYZ dan buktikan kesehatannya. Buktikan teorema parametrik untuk XYZ generics. Tambahkan tipe dependen untuk XYZ dan buktikan tipe-kesehatan. Kembangkan inferensi tipe parsial untuk tipe dependen XYZ. Tambahkan tipe bertahap untuk XYZ dan buktikan tipe-kesehatan. Tambahkan kontrak untuk XYZ. Masing-masing adalah kertas. Anda dapat berhenti jika mahasiswa PhD atau postdoc Anda kehabisan waktu. Masing-masing di atas menarik dan akan menghasilkan wawasan tentang obat generik, parametrik, inferensi jenis dll. Pipa ini baguscara menavigasi perairan yang sulit dari semua bahasa pemrograman yang mungkin. Cara belajar kedua adalah menerapkan bahasa dalam kompiler, tapi itu kurang bisa ditelusuri untuk seorang individu.

Apakah PLT dibutuhkan adalah pertanyaan yang menarik. Kebanyakan programmer yang bekerja sepertinya berpikir itu bukan. Mereka salah: sebagian besar bahasa dikembangkan oleh programmer yang bekerja tanpa latar belakang PLT (misalnya Javascript, PHP) mulai mengerikan, dan membuat semua kesalahan yang telah dipelajari oleh ahli teori PL bagaimana cara menghindarinya. Jika PL yang dikembangkan oleh seorang amatir mencapai arus utama, teoritikus PL perlu satu dekade atau lebih untuk memperbaiki kekurangan yang sudah jelas (misalnya, memasang kembali sistem pengetikan statis, lihat Skriptrip). Biarkan saya meringkas situasi ini:

 Every successful programming language ends up being ML! Either because 
 it was designed by a PL theorist as ML from the start, or because a 
 decade of painful evolution removes all the obvious flaws, leaving ML. ;-)

^{Selain itu: Keadaan ini sepenuhnya merupakan kesalahan PLT karena karena kebanyakan dari mereka tidak memiliki pengalaman pemrograman industri, jadi tidak benar-benar tahu apa yang menyakitkan dari para insinyur perangkat lunak yang bekerja. Secara khusus, untuk alasan sosiologis, sebagian besar teoritikus PL berpikir bahwa pemrograman fungsional murni dalam bahasa seperti Agda adalah solusi untuk semua masalah, yang tidak tahan terhadap pengawasan.}