TLA: menos que más, lo poco que nos dijo Lamport

El día de ayer el connotado creador de LaTeX, Leslei Lamport de paso por Chile dio una charla plenaria en el Departamento de Ciencias de la Computación de la Universidad de Chile, aclarando que este es uno de los centros de investigación y departamento en el área más solventes académicamente en Chile y en el contexto latinoamericano. Su charla titulada ¨How to write a proof?¨ más que ser una introducción a un nuevo paradigma, fue un intento por seducir sin el sex-appeal y así proponernos su enfoque materializado en su proyecto lenguaje TLA: Temporal Logic of Actions, que es y no es más como él mismo lo presenta un lenguaje formalizado para la especificación de demostraciones. Su presentación fue un itinerario desde lo que el denomino la escritura de demostraciones del Siglo XVII, pasando por la del siglo XX y dándonos los retazos formales de su propuesta para la escritura del siglo XXI, más de alguien se sintio aludido a que aquí en Chile aun hacemos las cosas como si estuviesemos en el siglo XVII. Creo que para todos los que estuvimos allí, sentimos  desde su rectus una no despreciable cuota de condescendencia. Pasando por el alto el tono de su discurso,  no nos queda más preguntarnos lo pertinente, y que para mi tiene que ver con resolver la relación existente entre la propuesta de Don Leslie y otros propuesta ya existentes, la  respuesta PhD. Lamport fue poco alentadora y peor aún displicente al comentar que el camino recorrido por esta alternativas, me refiero con ellas a lo que hoy por hoy se conoce como el enfoque de los sistemas MetaMath y que son los vástagos para  esta nueva centuria que comienza de los formalismos no-clasicistas tales como intuicionista y constructivistas . Creo que puedo comentar que para pesar de Lamport estas nuevas comunidades, aquellas que crecen alrededor de los asistentes de demostraciones, o mejor dicho proof assistants, cuentan con una serie de éxitos importantes a su haber, que por lo que pude constatar Mr. Lamport y su TLA no han logrado emular, entonces ¿Por qué subestimar otros enfoques? La respuesta de Lamport fue nuevamente condescendiente refiriéndose a que estas ventajas, aquellas que poseen los enfoques basados en las lógicas minimalistas serán finalmente superadas y que estas tienen fecha de termino, que al finalizar esta centuria, aquellas ventajas tales como eficiencia computacional serán alcanzadas por el enfoque clásico y que este superaría en definitiva a este referente alternativo gracias a la fuerza bruta obtenida desde las nuevas generaciones de máquinas. De sus comentarios sólo puedo desprender un postura conocida y tristemente celebre entre científicos, y esta es que mientras el músculo de la producción sea tonificado se nos permitirá alcanzar y superar cualquiera de las metas y dificultades que se nos pongan por delante. Me temo Sr. Lamport que la historia nos deparará una aventura mucho más entretenida y excitante de lo que usted conjetura, hemos visto como un sinfín de artefactos sofisticados pero finalmente inútiles cuelgan de las galerías de los museos.