Un programa informático, como podría ser Microsoft Word, requiere de actualizaciones periódicas para solucionar errores. Detectar y solucionar problemas de manera manual es un trabajo ingente: lento y costoso. Por este motivo, surgen sistemas que permiten que las comprobaciones se hagan de manera automática, sin necesidad de que un programador intervenga.
La informática es un campo amplio con dos polos: el teórico y el práctico. Los tipos de refinamiento pretenden fusionar estos dos polos y permitir que la programación convencional disfrute de algunas ventajas. Proporcionan una forma atractiva y automatizada de verificación formal utilizada para comprobar que las aplicaciones del mundo real son correctas, como por ejemplo, que una aplicación web no filtre información privada del usuario. Sin embargo, actualmente los tipos de refinamiento no proporcionan ninguna prueba matemática que compruebe la ausencia de fugas de información privada.
El proyecto liderado por Niki Vazou, CRETE (Certified Refinement Types) está diseñando un sistema sólido y práctico de tipos de refinamiento para que el desarrollo de programas sea más rápido, más seguro y esté libre de errores.
Además, CRETE pretende que la verificación formal sea tan atractiva que pueda utilizarse como ayuda en los cursos de programación y promover la programación verificada como la forma de facto de enseñar a programar.
