211service.com
Código Garantizado
Ariel Davis
Adam Chlipala, profesor asociado de ciencias de la computación en el MIT, cree que hay una forma mejor de escribir programas de computadora.
La mayoría de los programas simplemente enumeran las operaciones que la computadora debe realizar cuando recibe determinados tipos de datos. El programador tiene que escribir pruebas para determinar si un programa hace lo que se supone que debe hacer, y dado que es prácticamente imposible predecir todas las formas en que se puede usar un programa, la mayoría del software tiene errores.
Chlipala prefiere la llamada programación funcional. En lugar de encadenar comandos imperativos, un programador funcional define un conjunto de funciones o relaciones matemáticas entre entradas y salidas. Esencialmente, la programación funcional expresa lo que hace un programa como un conjunto de ecuaciones.
Pensar en los programas como combinaciones de funciones puede ser poco intuitivo, pero para las personas para las que funciona, es realmente un increíble potenciador de la productividad, dice Chlipala. Por un lado, puede eliminar las pruebas. Los programas funcionales son tan matemáticamente precisos que es relativamente simple verificarlos, o probar que hacen lo que deberían, automáticamente.
Uno de Chlipala principales intereses de investigación está ampliando el alcance de la verificación automática. Por ejemplo, las herramientas de verificación que él y sus colegas desarrollaron permitieron crear el primer sistema de archivos, la parte de un sistema operativo que gobierna el almacenamiento de datos, con la garantía de no perder los datos del programa durante un bloqueo del sistema.
Otra ventaja de los lenguajes funcionales es que eliminan gran parte del trabajo duro de la programación. Nuevamente, debido a que los programas funcionales son tan precisos, es fácil para los compiladores, los programas que convierten el código en archivos ejecutables, descubrir cómo hacer que se ejecuten de manera más eficiente.
Una de las herramientas más populares de Chlipala es un lenguaje funcional llamado Ur/Web, el único lenguaje de programación que permite a los programadores especificar toda la funcionalidad de una aplicación web en un solo programa. El compilador de Ur/Web genera automáticamente el código XML, el código JavaScript y las consultas de la base de datos necesarias para implementar la aplicación. También asegura que estos diferentes componentes interactúen correctamente.
Ur/Web es similar a otros lenguajes funcionales, pero agrega características de seguridad que le permiten tapar automáticamente los agujeros comunes en las aplicaciones web. Por ejemplo, puede garantizar que una parte de su código importado en una sección de una página (como un anuncio) no pueda espiar a otra (como una herramienta de calendario).
Como muchos científicos informáticos en sus 30, Chlipala había intentado escribir videojuegos en la escuela secundaria. Pero esa empresa rápidamente lo llevó en una dirección diferente. Cuando era estudiante de primer año, sus intentos de escribir juegos para la calculadora gráfica de Texas Instruments lo llevaron a desarrollar un compilador para el dispositivo.
Continuó enfocándose en compiladores como estudiante universitario en la Universidad Carnegie Mellon, y en su primer semestre como estudiante de posgrado en la Universidad de California, Berkeley, su futuro asesor de tesis le preguntó si le gustaría contribuir a un proyecto sobre computación. verificación asistida. Chlipala se enganchó de inmediato.
Hay un cierto tipo de personalidad paranoica que se vuelve adicta a este tipo de trabajo, y ese definitivamente soy yo, dice. No hay muchas cosas que sean absolutamente seguras en este mundo, pero cuando haces pruebas verificadas por máquina sobre programas, te acercas bastante.