El language matemático y los lenguajes de programación

(Del libro Théories des Types de Gilles Dowek)

Recientemente, la constitución de una lista de lenguajes de programación ha permitido enumerar mas de dos mil. Más de dos mil lenguajes concebidos en cuarenta años (desde la aparición del Fortran, propuesto por John Backus y su equipo), lo que significa una media de más de un lenguaje por semana. Desde luego, todos estos lenguajes no pueden ser puestos en el mismo plano: algunos están muertos desde hace tiempo, otros se reservan para aplicaciones muy puntuales, pero  la impresión que da la Informática es a menudo la de una torre de Babel poco acogedora.

Esta proliferación cuesta cara a la industria del Software: hace difícil la concepción de sistemas integrando módulos ya desarrollados en lenguajes diferentes, demanda la creación de interfaces, pasarelas y otros traductores y hace del mantenimiento de estos sistemas híbridos un verdadero rompecabezas. Para poner fín a esta discordancia, el ministerio de defensa de los EEUU puso en marcha, en 1978, un concurso con el fín de elegir un lenguaje de programación único para imponerlo como lenguaje de desarrollo para todo su software. Con esta idea de un "esperanto" de la programación, el ministerio de defensa americano se reencontraba con el sueño secular de una lengua artificial, perfecta y universal. Lengua que el teólogo Raymundo Lulio había ya intentado construir en el siglo trece. Este concurso (retomado al año siguiente por un equipo dirigido por Jean Ichbiah) permitió la creación del lenguaje Ada, el cual es todavía bastante popular, pero que ha fracasado en su vocación de universalidad.

No obstante, limitado al dominio restringido de la programación, este sueño de un lenguaje universal no debería considerarse utópico. La gran mayoría de los músicos utilizan el mismo lenguaje para escribir sus partituras. Análogamente, los matemáticos de todos los paises utilizan un lenguaje común, lo que no le impide a este lenguaje el evolucionar en función de las necesidades, ni que cada uno lo utilice con un estilo propio. Si en el dominio de la programación no hemos alcanzado aún esa unidad, ello puede ser una señal de que no hemos comprendido bien aún qué es un programa o un lenguaje de programación.
 

 ¿Qué es un programa?

Los manuales de iniciación a la programación suelen comenzar por explicar que un ordenador es una máquina capaz de tratar la información de maneras muy diversas (al contrario de la máquina de Pascal que era buena sólamente para efectuar sumas y restas) pero que se le debe de explicar antes al ordenador qué es lo que debe hacer y cómo debe hacerlo. Esta explicación, que se denomina programa, se expresa en un lenguaje especial, un lenguaje de programación. Por ejemplo, cuando se pide a un banco un préstamo para comprar un automóvil, éste utiliza un programa para calcular el importe de las mensualidades del préstamo en función de la suma prestada, del número de mensualidades y de la tasa de interés. Este programa utiliza la fórmula bien conocida:

donde f(e,n,t) es el importe de las mensualidades, e la cantidad prestada, n el número de mensualidades y t la tasa de interés mensual.

    Un programa es pues cualquier cosa que permite asociar una magnitud (el valor de salida) a una o varias magnitudes (los valores de entrada). Un tal objeto que permite asociar una magnitud a otras magnitudes es lo que los matemáticos denominan una función. El programa que utiliza el banco no es otra cosa que la función f que asocia el número  a los números e, n y t. Desde este punto de vista, un lenguaje de programación no es otra cosa que un lenguaje de definición de funciones.

    La necesidad misma de concebir  lenguajes de programación se encuentra entonces puesta en cuestión: si no se trata más que de definir funciones ¿para qué crear un nuevo lenguaje, dado que el lenguaje matemático ordinario lleva haciendo esto tan bien desde hece varios siglos?
 

Las funciones en el lenguaje matemático


Esta es la forma cómo los matemáticos definen la función que a un número le asocia su cuadrado: el término x´x indica el valor asociado por la función al valor x. El valor que toma f en 3, por ejemplo, se obtiene reemplazando el argumento formal x por el argumento real 3 en ese término, lo cual da 3 ´ 3.
    Esta notación existe casi literalmente en la mayor parte de los lenguajes de programación. Por ejemplo, en el lenguaje Pascal, concebido en 1970 por Niklaus Wirth y su equipo, se define esta misma función por el texto:

function f (x:integer) : integer;
begin
    f:= x*x
end;

    Pero, las funciones que se pueden definir explícitamente forman una pequeña parte de las funciones que se necesitan en matemáticas o informática. Por ejemplo, la función potencia que asocia el número a los números x y n no se puede definir explícitamente. En la escuela hemos aprendido que esta función tiene la curiosa definición:

Estos mismos puntos suspensivos han sido utilizados más tarde, cuando hemos aprendido ls definición de la función Seno que era:

Los puntos  suspensivos que se utilizan en estas dos definiciones no tienen en absoluto el mismo significado: en la de la definición del Seno expresan una definición como límite de una serie mientras que en la de la función potencia expresan una definición recursiva:

potencia(x,0)=1
potencia(x,n+1)=x´ potencia(x,n)

Dicho de otra forma, la función potencia se define como la única función verificando estas dos ecuaciones.
 

  • Se dan las propiedades que la función debe verificar:
  • Se demuestra que existe una única función que satisface estas propiedades.

  •  
  • Se atribuye el nombre  a la función.
La definición de la raiz cuadrada

 

    Sin embargo, no es suficiente dar un sistema de ecuaciones para definir una función. Así la ecuación

f(x)=f(x)

no es una definición correcta pues esta ecuación la verifican  muchas funciones. Analogamente la ecuación

f(x)=1+f(x)

no es tampoco una definición correcta pues no la verifica  ninguna función. La definición de la función potencia no será pues correcta hasta que se demuestre que existe una función única que verifique sus ecuaciones.
    Se comprende mejor entonces el mecanismo verdaderamente utilizado para definir funciones en matemáticas. Se comienza par dar un sistema de ecuaciones, o más generalmente una propiedad, que debe verificar la función, se muestra a continuación que existe una única función que verifica esa propiedad, y se da finalmente un nombre a la función.
    Para atribuir un nombre a la función se utiliza en general una frase de la forma "se llamará potencia a la única función que verifica las siguientes propiedades ..." Salvo su nombre, no hay ninguna expresión para designar la función en cuestión. Desde un punto de vista más formal (que es el propio de los que tratan de concebir lenguajes de programación) se puede denotar [f | P(f)] el único objeto que verifica la propiedad P de la misma manera que se denota {f | P(f)} el conjunto de los objetos que verifican esta propiedad. Esta notación que permite expresar un objeto por medio de una descripción se llama operador de descripciones.
    La función potencia se definiría pues como:

    Del mismo modo que la gramática del lenguaje matemático prohibe formar la expresión 1/0 que no tiene sentido, prohibe también la utilización del operador de descripciones con una propiedad que no es verificada por ningún objeto. Es, por ejemplo, imposible formar la expresión . (De hecho, no es esencial que estas expresiones carentes de sentido sean prohibidas por la gramática. Se puede adoptar también la convención según la cual la expresión 1/0 es correcta y designa un objeto matemático cualquiera: el conjunto vacío, el número 0, ... lo que importa es que la propiedad x´1/x = 1 sea verdadera únicamente cuando x sea diferente de 0).
    Cuando varios objetos verifican la propiedad utilizada, se pueden adoptar distintas convenciones. La utilización del operador de descripciones está, en general, prohibida en este caso, pero una regla más liberal autoriza esta utilización y permite, por ejemplo, la formación de la expresión [x | x´x = 9] que ya no se lee "el número x tal que x´x = 9" sino "un número x tal que x ´x = 9". El operador de descripciones se llama entonces operador de elección, operador e  de Hilbert o operador t de Bourbaki. El número [x | x ´x = 9] vale 3 ó -3, sin que se sepa si vale 3 ó -3. Así, no se puede demostrar [x | x ´x = 9]=3 ni [x | x´x = 9]=-3 pero se puede demostrar [x | x´x = 9{3,-3}.
 

Las especificaciones y los programas


Cuando un cliente demanda un programa a un informático, le debe explicar lo que debe hacer ese programa. Esta  explicación se llama el cuaderno de carga o también la especificación del programa. Por ejemplo, cuando un industrial pide a una sociedad de servicios un programa de inversión de matrices, la especificación cabe en una línea

f(M)´M = I
mientras que el programa puede ser mucho más largo.
    Si se adopta el lenguaje matemático como lenguaje de programación, la construcción de un programa a partir de su especificación P resulta muy fácil: el "programa" [f | P(f)] responde, por definición a la especificación P. Por ejemplo, el "programa"  es un programa de inversión de matrices. Además, este programa es automáticamente un programa sin errores, dado que no es más que una reformulación de su especificación. Programar en lenguaje matemático es pues, entre otros, un medio de concebir programas sin errores.

La ejecución de los programas

Cuando se ha terminado un programa, es preciso poder ejecutarlo. Así, si se prestan 30 000 Francos a 24 meses a un interés mensual de 0.64% ( lo que corresponde a una tasa anual del 8%), el programa mencionado antes debe indicar que las mensualidades serán de 1353 Francos. En efecto

f(30000,24,0.0064)=1353
El valor de la salida de un programa es pues una expresión E (en este ejemplo 1353) tal que la proposición
f(30000,24,0.0064)=E
sea verdadera. Pero ¿es esto suficiente? La proposición
f(30000,24,0.0064)=3´11´41
es también verdadera, y
f(30000,24,0.0064)=f(30000,24,0.0064)
también. Sin embargo no sería admisible el aceptar un préstamo sabiendo que el montante de las mensualidades es 3´11´41 Francos. Un abismo separa la expresión 1353 (que provee una información utilizable) de las expresiones 3´11´41 ó f(30000,24,0.0064). Una expresión, como 1353, en la que no hay nada que calcular es lo que en informática se llama un valor. El valor de un número entero es, por ejemplo, su representación decimal. El valor de un número racional puede ser su escritura bajo la forma de una fracción irreducible, o bajo la forma de una descripción de su desarrollo decimal periodico por una parte inicial y un período. Parece que no se puede asociar así una expresión única a los números reales, a los conjuntos o a las sucesiones de números enteros. Por el contrario, se sabe hacerlo para sucesiones y conjuntos finitos. Un conjunto donde todo elemento tiene un valor se llama un tipo de dato.
    Los matemáticos mantienen una actitud ambigua respecto a esta noción de valor. Desde un cierto punto de vista, cuando se le pide a un estudiante efectuar la suma 12+23, se espera el resultado 35 y no 10+25. Sin embargo, el mismo estudiante escribe 12+23=35, utilizando el signo "=" que es perfectamente simétrico. Existen de hecho dos tradiciones que coexisten en las matemáticas. Desde el punto de vista denotacional, las expresiones 12+23 y 35 designan el mismo objeto, lo que se expresa por la proposición 12+23=35. En esta proposición las expresiones 12+23 y 35 juegan papeles simétricos. Por el contrario, desde el punto de vista operacional hay una disimetría total entre la expresión 12+23 que es una pregunta y 35 que es la respuesta a esta pregunta. El drama de la informática es que el punto de vista operacional, que es el de los matemáticos de la antigüedad centrados entorno a los métodos operatorios, ha sido poco a poco axfisiado, en el curso de la historia, por el punto de vista denotacional. El desarrollo de la informática nos obliga hoy a reencontrarnos con esta tradición operacional.
    Nos es necesario pues concebir un lenguaje matemático que permita no solamente demostrar que 12+23=35 sinó también  transformar la expresión 12+23 en la expresión 35. La gramática del lenguaje matemático no debe dar únicamente reglas de razonamiento, sinó también reglas de cálculo, estas reglas que permiten transformar una expresión en otra se llaman reglas de reescritura. La regla de reescritura más simple (aunque tenga el nombre bárbaro de b-reducción) se utiliza para las funciones definidas explícitamente. Consiste en reemplazar los argumentos formales por argumentos reales. Así cuando se aplica la función a los números 3 y 4, se obtiene la expresión ()(3,4) que se calcula reemplazando x por 3 e y por 4 en la expresión x, dando el resultado de 3. El problema, que hace que tengamos necesidad de inventar los lenguajes de programación, es que no conocemos una regla semejante para las funciones definidas implícitamente por medio del operador de descripciones.
 

Algunos lenguajes de programación


Los lenguajes de programación tradicionales no proponen pues directamente operador de descripciones, sinó que proponen construcciones más restringidas que corresponden a casos particulares de utilización de este operador.
    Casi todos los lenguajes de programación permiten definir funciones por recurrencia con la ayuda de bucles. Así, en Pascal, se puede definir la función potencia por el bucle:

r:= 1; for i:=1 to n do r:=x*r

la ejecución de un tal programa demanda repetir n veces la operación que se encuentra en el bucle, es decir el calcular sucesivamente .
    Otros lenguajes, como el lenguaje Lisp (concebido en 1962 por John Mc Carthy y su equipo) o su sucesor el lenguaje ML (sugerido en 1966 por Peter Landin y concebido en 1978 por Robin Milner y su equipo) proponen la utilización de definiciones recursivas, es decir, simular la utilización de la función a definir en su propia definición. Por ejemplo, en ML, se define la función potencia así:

let rec potencia = fun x n -> if n=0 then 1 else x*(potencia x (n-1));;

Como es incorrecto definir un objeto utilizando el mismo objeto a definir, un tal programa debe entenderse como una definición implícita utilizando el operador de descripciones:

Definir así las funciones recursivamente significa utilizar el operador de descripciones en el caso particular donde las propiedades son de la forma f = G(f). Ejecutar un tal programa exige ejecutar el cuerpo de la definición G(f) llamando a la función misma cuando se utiliza en la propia definición.
    Contrariamente a los bucles, este mecanismo permite salir de los límites de utilización del operador de descripciones autorizado por la gramática del lenguaje matemático (lo cual impone que existe un único objeto verificando la propiedad). Así los programas en ML:

let rec f = fun x -> f x;;

let rec f = fun x -> 1 + (f x);;

corresponden a las definiciones "ilegales" . Esto se traduce en el hecho de que la ejecución de estos programas lleva a cálculos infinitos (calcular f(0) demanda calcular antes f(0) lo cual exige calcular antes ....). Para dar un sentido a estas definiciones recursivas incorrectas, Dana Scott propuso en 1970 añadir al espacio de valores, un valor suplementario "indefinido" y ver las definiciones recursivas como funciones sobre este espacio de valores extendido, las dos definiciones anteriores se convierten en "legales" y corresponden a la misma función constantemente igual a ese valor "indefinido", Dicho de otro modo, la ejecución de estos dos programas sobre cualquier entrada lleva siempre a cálculos infinitos.
    A diferencia del lenguaje ML que utiliza el operador de descripciones para definir la función misma, el lenguaje Prolog (concebido en 1973 por Alain Colmerauer y su equipo) utiliza el operador de descripciones únicamente para definir el valor tomado por la función, es decir, el valor de salida del programa. Por ejemplo la función potencia no será ya definida por un término de la forma [f  | P(f)] donde P es una propiedad característica de esta función, sino por un término de la forma
siguiente :

donde Q es una propiedad característica del número . La propiedad  Q(x,n,y)  puede ser, por ejemplo:

que recuerda al programa en prolog

e(A,0,1).
e(A,P,S) :-  Q is P-1, e(A,Q,R), S is A*R.

Le ejecución del programa demanda resolver la ecuación Q(x,n,y) en y. Esta ecuación al tratar sobre un valor y no sobre una función, se puede resolver de una forma bastante sistemática.
    Más generalmente los lenguajes de programación con restricciones introducidos por Joxan Jaflar y Jean-Louis Lassez en 1987 son extensiones del Prolog que utilizan algoritmos especiales para la resolución de estas ecuaciones.
 
 

Las funciones no calculables


Se pueden ver pues los lenguajes de programación tradicionales como restricciones del lenguaje matemático. El operador de descripciones no se utiliza más que en ciertos casos particulares, la restricción escogida distingue unos lenguajes de otros. La ventaja de esta restricción es que permite ejecutar los programas. Su inconveniente es que limita la expresividad de los programadores. Un lenguaje de programación es siempre un compromiso entre la potencia de la expresión y la posibilidad de ejecución.
    La cuestión que se puede entonces proponer es la de saber si es posible encontrar reglas de cálculo para la totalidad del lenguaje matemático, es decir, para el operador de descripciones en toda su generalidad. La respuesta negativa a esta pregunta la da la teoría de la calculabilidad: un resultado debido a Alan Turing e independientemente a Alonzo Church y Stephen Kleene, en 1936, demuestra, en efecto, que existen funciones que no son calculables. El ejemplo más célebre de función no calculable es el problema de la parada: el imposible construir un programa que tome como entrada otro programa e indique si lleva a cálculos finitos o infinitos. Se puede pues definir la función

h = [f | para todo p, si  p  termina entonces f(p)=0  y sinó f(p)=1]

pero no hay regla de cálculo que nos dé sistemáticamente el valor de h(p).
    Para que esta definición sea correcta, es preciso demostrar que una única función verifica la especificación. Esta demostración utiliza el hecho de que para todo programa p, o bien p termina o bien p no termina. Este hecho es, él mismo, establecido por una regla de razonamiento, el tercio excluso, que indica que para toda proposición P se puede demostrar "P o no P" sin saber demostrar "P" ni "no P".
 

 
Un ejemplo de razonamiento rechazado por los intuicionistas es el siguiente. Se desea demostrar que existen dos números irracionales x e y tales que sea racional. Se razona así: El número  es racional o irracional.
  • Si es racional, se toma x = y .Los números x e y son irracioanles y  es racional por hipótesis.

  •  
  • Si es irracional se toma xy.El número x es irracional por hipótesis, y es irracional y  = 2 que es racional.
Este razonamiento no es válido para los intuicionistas pues no se puede suponer que el número  es racional o irracional sin demostrar primero o bien que es racional o que es irracional.

Un ejemplo de razonamiento no constructivo

    Al comienzo del siglo veinte, una escuela de matemáticos, llamados intuicionistas o constructivistas, han criticado vívamente esta regla de razonamiento. ¿Cómo puede pretenderse saber que la proposición "P o no P" es cierta, si no se sabe ni que "P" es cierta, ni que "no P" es cierta? Del mismo modo, ¿cómo se puede pretender haber definido el número h(p) si no se sabe si este número vale 0 ó 1? Para los intuicionistas la definición de la función h de antes  es simplemente incorrecta. Detrás de Luitzen Egbertus Jan Brouwer, el jefe de filas de la escuela intuicionista, forman matemáticos importantes como Hermann Weyl o Andreï Kolmogorov.
    Un teorema de Setphen Kleene demuestra que, cuando se abandona el tercio excluso, todas las funciones que se pueden definir con el operador de descripciones son calculables. Este teorema toma naturalmente formas diferentes en función de la teoría en la que se coloca para demostrar la existencia y la unicidad de la función descrita. Dicho de otro modo, el tercio excluso es indispensable para demostrar la existencia de una función no calculable. Cuando se abandona el tercio excluso, entonces es posible encontrar reglas de cálculo para el operador de descripciones en toda su generalidad. Cuando se define una función [f | P(f) ] después de haber dado una demostración constructiva p de la existencia de una función verificando la propiedad P, se puede ejecutar ese programa. Para ello se aplica a la demostración p y al valor de entrada, una transformación llamada eliminación de cortaduras. El primer procedimiento de eliminación de cortaduras ha sido propuesto en 1934 por Gerard Gentzen para las demostraciones expresadas en la aritmética. Después, se ha generalizado a muchas otras teorías. En particular, Jean-Yves Girard propuso en 1971 un procedimiento de eliminación de cortaduras para la aritmética de orden superior, que es una variante de la teoría de conjuntos.
    Aparece entonces una nueva metodología de la programación: se comienza por especificar la función a programar por una propiedad P, se da a continuación una demostración constructiva p de la existencia de una función que verifica esta propiedad y se define a continuación el programa [f | P(f)]. La ejecución de este programa consiste en eliminar las cortaduras en la demostración p. Esta aproximación es la base del lenguaje AF2 sugerido por Daniel Leivant y concebido por Michel Parigot en 1987.
 

Las demostraciones como objetos

Si este lenguaje permite la utilización del operador de descripciones bajo una forma muy general, como contrapartida abandona el principio según el cual un programa es una función matemática ordinaria: no es la función [f | P(f)], sinó la demostración p, lo que se utiliza para la ejecución del programa.
    Más generalmente, en el lenguaje matemático tradicional, el estatuto de la demostración p respecto a la expresión [f | P(f)] no está completamente claro. Si la expresión [f | P(f)] es incorrecta cuando no hay ningún objeto cumpliendo la propiedad P, ¿cuando es preciso demostrar la existencia de un tal objeto? ¿a la primera aparición de esta expresión? ¿cada vez que aparece? ¿para demostrar que el objeto [f | P(f)] verifica la propiedad P? ¿después de haber utilizado esta expresión en una demostración? ¿La propia demostración p forma parte de todas las demostraciones que utilizan una expresión de la forma [f | P(f)] ? El lenguaje matemático tradicional elude estas cuestiones utilizando, para definiciones implícitas, un proceso en tres tiempos que mezcla expresión de la propiedad, demostración de la existencia del objeto y atribución de un nombre.
    Para resolver, entre otras,  estas cuestiones, Per Martin-Löf propuso en 1973, en su Théorie des types intuitioniste dar a las demostraciones un estatus de objetos matemáticos de pleno derecho, comparable al de los números o las funciones. La teoría de tipos intuicionista es una extensión del lenguaje matemático habitual en el cual se puede hablar no solo del número 2 (por ejemplo, para decir que es par) sinó también de la proposición "2 es un número par" y de su demostración p.
    En esta teoría y en sus extensiones, como el Cálculo de Construcciones propuesto en 1985 por Thierry Coquand y Gérard Huet, una función no está definida solamente a partir de una propiedad que ella debe satisfacer, sinó igualmente a partir de una demostración de la existencia de una función verificando esta propiedad. No se escribe pues ya [f | P(f)], sinó [f | P(f),p]. Así el estatuto de la demostración p queda clarificado: es una componente de la expresión [f | P(f),p]. La gramática del lenguaje matemático prohibe entonces la formación de la expresion [f | P(f),p] cuando p no es una demostración de la existencia de un objeto que verifique la propiedad P, pero esta propiedad es entonces decidible y no exige pues ser argumentada. En estas teorías, las demostraciones son funciones definidas explícitamente, pero en un lenguaje extendido.
    En estas teorías, la función [f | P(f),p], conteniendo la demostración p, contiene la información de la marcha a seguir para su ejecución. Se reencuentra así a la vez la posibilidad de definir programas como funciones ordinarias y la de ejecutar estos programas eliminando las cortaduras en la demostración p.
    Programar en estos lenguajes consiste en tomar la especificación P dada por el cliente y devolverle el programa [f | P(f),p]. Naturalmente, esto exige construir la demostración p de la existencia de una función que verifica la especificación, lo que es un verdadero trabajo de programación. Una ventaja es que si esta demostración es correcta (lo que es una propiedad decidible), el programa [f | P(f),p] verifica, por definición, esta especificación y es por lo tanto un programa sin errores..
 

La gestión de los recursos

Para ser realmente competitivo respecto a las aproximaciones más tradicionales, la programación en lenguaje matemático deberá sin duda resolver aún el problema de la gestión de los recursos. Desde la aparición de los primeros lenguajes de programación, los programadores tienen el sentimiento de ser desposeidos del control de las operaciones efectuadas en sus máquinas. Por ejemplo, utilizando nombres simbólicos para designar las variables del programa, han tenido la sensación de perder el control de la dirección donde realmente estaba guardada la información en la memoria. Este sentimiento es tanto más vivo cuanto más alto nivel tiene el lenguaje utilizado, pero toma posiblemente una forma nueva cuando se programa en lenguaje matemático. En efecto, para ordenar por orden alfabético una lista de palabras, por ejemplo la lista: whisky, gin, vodka, un programa permuta, por ejemplo, las palabras whisky y gin para construir la lista gin, whisky, vodka, después whisky y vodka para construir la lista gin, vodka, whisky,. Si el programa guarda en memoria las tres listas:

whisky, gin, vodka
gin, whisky, vodka
gin, vodka, whisky

es un programa mal concebido. Todos los programadores saben que la primera lista es inútil una vez que se construye la segunda y que por lo tanto se puede ordenar "en su propio espacio" es decir utilizando la misma zona de memoria para guardar los estados sucesivos de la lista.
    Si nos contentamos con demostrar la existencia de una función que asocia una permutación ordenada a cada lista ¿cómo saber si la ejecución de este programa ordenará las listas "en su propio espacio" o recopiará la lista en cada etapa? Las matemáticas no son un lenguaje de programación muy consciente de la gestión de los recursos.
    La programación en lenguaje matemático propone nuevos desafíos a las teorías de la compilación, del análisis estático y de la transformación de programas  ¿Cómo transformar un programa desarrollado en lenguaje matemático en un programa equivalente en lenguaje máquina  pero que gestione eficazmente sus recursos y no efectúe cálculos inútiles?
    Un útil esencial para resolver estas cuestiones es sin duda la lógica lineal, desarrollada por Jean-Yves Girard en 1987. Según esta teoría , las matemáticas no son muy conscientes de la gestión de los recursos porque "las hipótesis no se gastan cuando se utilizan". Así en las lógicas tradicionales las proposiciones "P" y "P & P" son equivalentes. En lógica lineal estas dos proposiciones no son ya equivalentes, suponer la primera permite utilizar una única vez la hipótesis P en una demostración mientras que suponer la segunda permite utilizar dos veces esta hipótesis. En la demostración de la existencia de una función de ordenación, una hipótesis utilizada una única vez revela que una vez que se ha utilizado la lista, puede destruirse, lo cual es exactamente la información necesaria para programar la ordenación "en place". La lógica lineal ya ha sido utilizada para gestionar los recursos en compiladores para el lenguaje ML. Este tipo de análisis debe ser extendido al caso de la programación en lenguaje matemático.
 

Reacciones al lenguaje matemático

La teoría de los lenguajes de programación permite pues explicar porqué el lenguaje matemático no se adapta completamente a la programación, en qué son los lenguajes de programación tradicionales restricciones del lenguaje matemático, y cómo es preciso modificar éste último para que sea posible su uso para programar.
    Desde la antigüedad, el lenguaje de los matemáticos ha evolucionado enormemente para responder a las necesidades de los matemáticos que han ido variando en el transcurso de la historia. Hoy, parece que el desarrollo de la informática sugiere una nueva evolución del lenguaje matemático.
    Naturalmente, una sugerencia de evolución del lenguaje matemático tendrá éxito únicamente cuando sobrepase el estrecho cuadro del problema que lo motive y cuando permita expresar las matemáticas en su conjunto. Como hemos visto, respecto a la teoría de conjuntos que es el lenguaje de las matemáticas del siglo veinte, las reformas que los informáticos sugieren hoy conciernen a tres puntos:
Parece que la vuelta hacia un punto de vista más operacional no significa un verdadero problema. Que 12+23 se calcule a 35 como hecho diferenciado de que sea igual a 35 es una idea largamente compartida. La toma en cuenta de las demostraciones como objetos matemáticos no parece proponer un verdadero problema. En el transcurso de la historia, los matemáticos han integrado siempre los objetos extramatemáticos que utilizaban. Las funciones que eran utilizadas desde la antigüedad para designar las magnitudes (por ejemplo en la expresión "Seno(0)") se convirtieron en objetos matemáticos de pleno derecho con Newton y Leibniz, y también con Euler, cuando se hizo posible expresar propiedades de las propias funciones (y decir que la función Seno es, por ejemplo, continua, periódica, derivable, etc.). Además, parece que tener las demostraciones como objetos de pleno derecho resuelve problemas fuera del campo de la programación, y en particular que ciertas formas del axioma de la elección aparezcan como teoremas.
    Es, desde luego, el abandono del tercio excluso lo que plantea más problemas. Abandonar el tercio excluso significa dejar de lado resultados importantes del análisis, por ejemplo el teorema según el cual una función continua sobre un intervalo cerrado toma un valor máximo. Más que de abandonar completamente los métodos no constructivos, parece que el desafío hoy en día sería concebir un lenguaje matemático que integre, distinguiendolos claramente, los argumentos constructivos  y los no constructivos.