Dado que:
- Un lenguaje con sistemas de tipos muy expresivos (por ejemplo, Idris ) también puede tener mecanismos de escape como interfaces de funciones foráneas / unsafePerformIO.
- Hay asistentes de prueba que pueden usarse para probar algunas propiedades de un programa escrito en un lenguaje que no tiene un sistema de tipos capaz de expresar esas propiedades.
- La correspondencia de Curry-Howard muestra que una implementación verificada con éxito de una función con un tipo dado es una prueba de lo que ese tipo expresa.
¿Se pueden expresar pruebas no triviales de alguna propiedad del código de idioma extranjero en el sistema de tipos del idioma nativo?
Por ejemplo, imagine que tengo una función C llamada stable_qsort que clasifica los números de una manera terriblemente inteligente y eficiente mientras mantiene el orden de elementos ya iguales, y un programa Idris que llama stable_qsort a través de su FFI, pero no confío en esto relativamente oscuro Función C. ¿Podría probar que la función no reordena elementos iguales, para todas las entradas, en mi código Idris en lugar de usar un asistente de prueba separado?