Na jakie „pytanie” stara się odpowiedzieć teoria języka programowania?

Od jakiegoś czasu interesowałem się różnymi tematami, takimi jak logika kombinacyjna, rachunek lambda, programowanie funkcjonalne i studiowałem je. Jednak w przeciwieństwie do „teorii obliczeń”, która stara się odpowiedzieć na pytanie „obliczalności”, tj. Rzeczy, które można / nie można obliczyć z różnymi ograniczeniami, staram się znaleźć analogię do „teorii programowania”

Wikipedia opisuje to jako:

Teoria języków programowania (PLT) to dziedzina informatyki, która zajmuje się projektowaniem, wdrażaniem, analizą, charakteryzacją i klasyfikacją języków programowania oraz ich indywidualnymi cechami.

To tak, jakby powiedzieć „wszystko”, co nie jest tak naprawdę konkretne.

Wspólny postęp tematów jest zwykle taki:

Logika kombinacyjna> Rachunek lambda> Teoria typów Lofda> Typowany rachunek Lambda> (coś się tutaj dzieje)> Opracowano języki programowania - które mają bardzo mały związek z CL /$\lambda$

Widzę leżącą u podstaw „matematykę” związaną z CL /$\lambda$i ciekawe dowody, które się w rezultacie ujawniają, w tym twierdzenie Church-Rosser i to jest fajne. Jednak staram się zrozumieć „cel końcowy” tego przedsięwzięcia? Jaki jest święty Graal PLT, jeśli chcesz? Na razie wydaje się, że to tylko drapanie intelektualnego swędzenia, ale tak naprawdę nie mogę przekroczyć mostu od badań / teorii do czegokolwiek praktycznego.

Uwaga: dostaję go do momentu użycia $\lambda$-calc dla dowodów nierozstrzygalności. Ale poza jego stosowalnością do „obliczalności” po prostu tego nie rozumiem i trudno mi nawet zrozumieć potrzebę badań nad PLT z tego wąskiego POV. Jakieś istniejące książki, odniesienia, które mogą rzucić światło na „duży obraz” PLT?

Ogólnym celem PLT jest uczynienie inżynierii oprogramowania przemysłowego (w sensie ogólnym) tańszym (również w sensie ogólnym) poprzez optymalizację najważniejszego narzędzia (języków programowania) i powiązanego ekosystemu narzędziowego.

Kilka powodów, dla których matematyka jest zaangażowana:

• PL są wysoce nietrywialne i nie jest jasne, czy postępują właściwie bez dowodów. Matematyka daje uproszczony model prawdziwych języków programowania. Ten model pozwala nam uczyć się prawdziwych języków programowania w znacznie uproszczonym ustawieniu, usuwając (mam nadzieję) większość problemów już na poziomie modelu. Prawdziwe języki programowania są obecnie matematycznie trudne. Innymi słowy: rachunek lambda to muszka owocowa, E.Coli, sferyczna krowa PLT.

• PLT nie ma odpowiednich metod empirycznych, które byłoby miło / lepiej mieć, więc matematyka jest wykonywana jako zamiennik.

• Matematyka jest piękna i głęboka.

• Matematyka podaje prostą, sprawdzoną metodologię badań, która jest ważna, aby pomóc doktorantom w ukończeniu studiów. Zazwyczaj niektóre warianty np .: Zbadaj PL zawierają XYZ poprzez dodanie go do rachunku lambda. Dodaj proste typy dla XYZ i udowodnij solidność tekstu. Dodaj generyczne dla XYZ i udowodnij poprawność tekstu. Udowodnij twierdzenie parametryczne dla generycznych XYZ. Dodaj typy zależne dla XYZ i udowodnij poprawność typów. Opracuj częściowe wnioskowanie o typach dla typów zależnych od XYZ. Dodaj stopniowe typy dla XYZ i udowodnij solidność tekstu. Dodaj umowy dla XYZ. Każdy z nich to artykuł. Możesz przerwać, jeśli doktorantowi lub postdocowi zabraknie czasu. Każde z powyższych jest interesujące i daje wgląd w informacje ogólne, parametryczne, wnioskowanie o typach itp. Ten potok jest świetnysposób poruszania się po trudnych wodach wszystkich możliwych języków programowania. Drugim sposobem uczenia się jest implementacja języków w kompilatorze, ale jest to mniej praktyczne dla osoby.

Czy PLT jest potrzebne, jest interesującym pytaniem. Wydaje się, że większość pracujących programistów uważa, że ​​tak nie jest. Mylą się: większość języków opracowanych przez pracujących programistów bez tła PLT (np. JavaScript, PHP) zaczyna się okropnie i popełnia wszystkie błędy, których teoretycy PL od dawna nauczyli się unikać. Jeśli PL opracowane przez amatora trafi do głównego nurtu, teoretycy PL potrzebują około dekady naprawienia oczywistych wad (np. Modernizacja statycznego systemu pisania, patrz Typescript). Pozwól, że streszczę tę sytuację:

 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. ;-)

^{Poza tym: ten stan rzeczy jest całkowicie winą PLT, ponieważ ponieważ większość z nich nie ma doświadczenia w programowaniu przemysłowym, więc tak naprawdę nie wiem, jakie są bolączki pracujących inżynierów oprogramowania. W szczególności, z powodów socjologicznych, większość teoretyków PL uważa, że ​​czyste programowanie funkcjonalne w językach takich jak Agda jest rozwiązaniem wszystkich problemów, co nie jest w stanie zbadać.}