Métodos Formales para el Razonamiento

Proyecto PAPIIT-IA105923 Métodos Formales para el Razonamiento 

El término Métodos Formales se refiere a un conjunto de metodologías, herramientas y formalismos que se dedican a la verificación del correcto funcionamiento de sistemas computacionales. Cada uno está enfocado en analizar características particulares de los sistemas o programas. Dentro de ellos se encuentran los sistemas de tipos, lógicas especializadas (Hoare, temporales, lineal, etc.), ambientes de desarrollo y demostración, etc.

La programación certificada es un marco teórico-práctico que permite obtener programas correctos por construcción. Esto significa que la especificación y la implementación de un programa se llevan a cabo al mismo tiempo dentro del mismo sistema, facilitando así la verificación de la segunda respecto a la primera. Los asistentes de prueba y los lenguajes de programación con tipos dependientes son los representantes de este estilo de programación.

Estas herramientas formales están basadas en el cálculo lambda y sus diferentes versiones ofrecen abstracciones particulares para múltiples nociones de cómputo. Así, la teoría de tipos simples se propone por un lado, como fundamento para el estudio semántico en filosofía del lenguaje y por otro lado, ser un componente principal del desarrollo y estudio de los lenguajes de programación. En particular el concepto de "composicionalidad", presente en muchas nociones de cómputo y mayormente en el estilo de programación funcional puede conformar un marco uniforme para estudiar aspectos semánticos del lenguaje además de favorecer competencias de estructura y organización del razonamiento en los procesos de desarrollo de software o sistemas computacionales (análisis, diseño, implementación, verificación).

El manejo de información en lógica entendido por el razonamiento puro deductivo de las demostraciones o derivaciones también es una herramienta que puede ofrecer maneras de abstracción y análisis no solo en el ámbito computacional sino también en el filosófico.

Un pilar fundamental en el quehacer computacional es el razonamiento formal, este puede favorecerse de los métodos formales ya que el marco que proveen es ideal para el análisis, desarrollo, implementación y verificación de sistemas computacionales para verificar diferentes objetivos así como su uso en diferentes etapas de estos procesos.

Dentro de los diferentes tipos de métodos formales podemos explotar aquellas herramientas matemáticas y computacionales para la verificación formal y que además ofrecen un marco uniforme para estudiar y resolver problemas tanto de las ciencias de la computación como en la filosofía del lenguaje.

Este proyecto busca acercar ambas disciplinas para encontrar coincidencias que favorezcan el desarrollo de herramientas adecuadas en el manejo de información (programas y datos) e iterpretaciones o lecturas para la semántica formal que den luz en la solución de problemas.

En particular, los diferentes cálculos lambda para modelar nociones de cómputo también pueden aplicarse a la formalización y argumentación. La correspondencia entre estos cálculos y los sistemas de tipos para lenguajes de programación tienen una contribución importante en el razonamiento computacional: ofrecer seguridad en el diseño e implementación de programas. Por otro lado, los asistentes de prueba contribuyen con un ambiente de desarrollo de demostraciones y de programación que caracteriza el razonamiento formal.