| La verificación basada en tipos tiene un alto potencial de ser adoptada en la industria, por múltiples razones. Primero, no apunta a la verificación de propiedades globales de un sistema completo. Aún con tipos dependientes, nunca es necesario establecer un teorema sobre el sistema en su globalidad. Solamente se expresan propiedades locales. La conexión lógica entre estas propiedades locales y las propiedades globales que se desean no se verifica. La experiencia con otras técnicas de verificación formal muestra que apuntar a verificar dicho razonamiento global es un tremendo esfuerzo, fuera del alcance para la mayoría de la industria del software. Segundo, los programadores ya están acostumbrados a desarrollar en lenguajes con tipos estáticos. Si bien los sistemas de tipos que se exploraron aquí son semánticamente bastante más ricos que los tipos tradicionales, la metodología de programación es muy cercana. No es necesario aprender un nuevo lenguaje de modelamiento o una nueva herramienta de análisis. La integración fuerte entre programar, especificar, y verificar es un factor de adopción importante. Podemos prever un escenario de adopción progresiva de estas técnicas de verificación, con sistemas de tipos con una semántica paulatinamente más rica. De hecho, este escenario ya se hizo realidad cuando Java adoptó el polimorfismo paramétrico en su versión 1.5, y ahora con el lenguaje Scala--cuyo sistema de tipos es mucho más avanzado que el de Java--que está progresivamente reemplazando a Java en muchas aplicaciones (p.ej. Twitter y LinkedIn). Además, es posible diseñar sistemas de tipos muy expresivos que sean graduales, con tal de que no sea necesario demostrar todas las propiedades a la vez, sino que se puedan dejar varias a cargo de una verificación dinámica, e ir elaborando la verificación estática paso a paso. | La verificación basada en tipos tiene un alto potencial de ser adoptada en la industria, por múltiples razones. Primero, no apunta a la verificación de propiedades globales de un sistema completo. Aún con tipos dependientes, nunca es necesario establecer un teorema sobre el sistema en su globalidad. Solamente se expresan propiedades locales. La conexión lógica entre estas propiedades locales y las propiedades globales que se desean no se verifica. La experiencia con otras técnicas de verificación formal muestra que apuntar a verificar dicho razonamiento global es un tremendo esfuerzo, fuera del alcance para la mayoría de la industria del software. Segundo, los programadores ya están acostumbrados a desarrollar en lenguajes con tipos estáticos. Si bien los sistemas de tipos que se exploraron aquí son semánticamente bastante más ricos que los tipos tradicionales, la metodología de programación es muy cercana. No es necesario aprender un nuevo lenguaje de modelamiento o una nueva herramienta de análisis. La integración fuerte entre programar, especificar, y verificar es un factor de adopción importante. Podemos prever un escenario de adopción progresiva de estas técnicas de verificación, con sistemas de tipos con una semántica paulatinamente más rica. De hecho, este escenario ya se hizo realidad cuando Java adoptó el polimorfismo paramétrico en su versión 1.5, y ahora con el lenguaje Scala--cuyo sistema de tipos es mucho más avanzado que el de Java--que está progresivamente reemplazando a Java en muchas aplicaciones (p.ej. Twitter y LinkedIn). Además, es posible diseñar sistemas de tipos muy expresivos que sean graduales, con tal de que no sea necesario demostrar todas las propiedades a la vez, sino que se puedan dejar varias a cargo de una verificación dinámica, e ir elaborando la verificación estática paso a paso. |
| Encontrar un sabio equilibrio entre la complejidad de la programación verificada y sus beneficios en términos de correctitud es un desafiante problema de ingeniería de software, que merece ser estudiado en profundidad. Dada la enorme dependencia de nuestra sociedad en los sistemas de software, es de esperar que la programación verificada se volverá una práctica común, contribuyendo ampliamente a la correctitud del software que usamos día a día. | Encontrar un sabio equilibrio entre la complejidad de la programación verificada y sus beneficios en términos de correctitud es un desafiante problema de ingeniería de software, que merece ser estudiado en profundidad. Dada la enorme dependencia de nuestra sociedad en los sistemas de software, es de esperar que la programación verificada se vuelva una práctica común, contribuyendo ampliamente a la correctitud del software que usamos día a día. |
