El propósito general de PLT es hacer que la ingeniería de software industrial (en un sentido general) sea más barata (también en un sentido general), mediante la optimización de la herramienta más importante (lenguajes de programación) y el ecosistema de herramientas asociado.
Algunas razones por las cuales las matemáticas están involucradas:
Los PL son altamente no triviales, y no está claro que hagan lo correcto sin pruebas. Las matemáticas dan un modelo simplificado de lenguajes de programación reales. Este modelo nos permite estudiar lenguajes de programación reales en una configuración mucho más simplificada, eliminando (con suerte) la mayoría de los problemas que ya existen a nivel de modelo. Los lenguajes de programación reales son actualmente matemáticamente intratables. En otras palabras: el cálculo lambda es la mosca de la fruta, el E. Coli, la vaca esférica del PLT.
PLT carece de métodos empíricos adecuados, lo cual sería bueno / mejor tener, por lo que las matemáticas se realizan como un sustituto.
Las matemáticas son hermosas y profundas.
Las matemáticas brindan una metodología de investigación simple, probada y de prueba, que es importante para ayudar a los estudiantes de doctorado a graduarse. Típicamente, alguna variante de, por ejemplo: Investigar la función PL XYZ mediante su adición al cálculo lambda. Agregue tipos simples para XYZ y pruebe la solidez de los tipos. Agregue genéricos para XYZ y pruebe la solidez del tipo. Probar un teorema de parametricidad para genéricos XYZ. Agregue tipos dependientes para XYZ y pruebe la solidez de los tipos. Desarrolle una inferencia de tipo parcial para los tipos dependientes de XYZ. Agregue tipos graduales para XYZ y pruebe la solidez de los tipos. Agregar contratos para XYZ. Cada uno de esos es un papel. Puede detenerse si su estudiante de doctorado o postdoctorado se queda sin tiempo. Cada uno de los anteriores es interesante y proporcionará información sobre genéricos, paramétrica, inferencia de tipos, etc. Esta tubería es una excelenteforma de navegar por las aguas difíciles de todos los lenguajes de programación posibles. Una segunda forma de aprender es implementar idiomas en un compilador, pero eso es menos manejable para un individuo.
Si se necesita PLT es una pregunta interesante. La mayoría de los programadores que trabajan parecen pensar que no lo es. Están equivocados: la mayoría de los lenguajes desarrollados por programadores que trabajan sin experiencia en PLT (por ejemplo, Javascript, PHP) comienzan terriblemente y cometen todos los errores que los teóricos de PL aprendieron durante mucho tiempo a evitar. Si un PL desarrollado por un aficionado llega a la corriente principal, los teóricos de PL necesitan una década más o menos para solucionar los defectos obvios (por ejemplo, actualizar un sistema de tipeo estático, ver Tipos de letra). Permítanme resumir esta situación:
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. ;-)
Aparte:
este estado de cosas es completamente culpa del PLT porque, debido a que la mayoría de ellos no tienen experiencia en programación industrial, entonces realmente no sé cuáles son los puntos débiles de los ingenieros de software que trabajan. En particular, por razones sociológicas, la mayoría de los teóricos de PL piensan que la programación funcional pura en lenguajes como Agda es la solución a todos los problemas, lo que no resiste el escrutinio.