Se ha dicho mucho sobre los efectos que la IA tendrá en el desarrollo de software, pero hay un ángulo del que no he visto que se hable: creo que la IA llevará la verificación formal, que durante décadas ha sido una práctica de nicho, al centro del desarrollo de software.
El título del artículo me hizo pensar que Martin se refería a verificación formal de identidad — es decir, ¿cómo verificas que lo que estás consumiendo fue hecho por un humano? Pero no, se refiere a la verificación formal de código:
Los asistentes de pruebas y los lenguajes de programación orientados a pruebas, como Rocq, Isabelle, Lean, F*, y Agda, existen desde hace mucho tiempo. Permiten escribir una especificación formal que cierto código debe cumplir, y luego demostrar matemáticamente que el código siempre satisface esa especificación (incluso en casos límite extraños que no se te habría ocurrido probar). Estas herramientas se han usado para desarrollar sistemas de software grandes y formalmente verificados, como un kernel de sistema operativo, un compilador de C y una pila de protocolos criptográficos.
Pero fundamentalmente está hablando del mismo concepto. En un mundo donde producir código es prácticamente gratuito, ¿cómo le haces para preservar el valor de código bien escrito?
La misma pregunta aplica para muchas otras disciplinas.
Deja un comentario