Un système de typage peut-il servir d'assistant de preuve pour des fonctions étrangères?

Étant donné que:

1. Un langage avec des systèmes de type très expressifs (par exemple Idris ) peut également avoir des mécanismes d'échappement comme des interfaces de fonctions étrangères / unsafePerformIO.
2. Il existe des assistants de preuve qui peuvent être utilisés pour prouver certaines propriétés d'un programme écrit dans un langage qui n'a pas de système de type capable d'exprimer ces propriétés.
3. La correspondance Curry-Howard montre qu'une mise en œuvre avec succès vérifiée par type d'une fonction avec un type donné est la preuve de ce qui est exprimé par ce type.

Peut-on exprimer des preuves non triviales d'une propriété du code de langue étrangère dans le système de type de la langue maternelle?

Par exemple, faites comme si j'avais une fonction C appelée stable_qsort qui trie les nombres de manière terriblement intelligente et efficace tout en maintenant l'ordre des éléments déjà égaux, et un programme Idris qui appelle stable_qsort via son FFI, mais je ne fais pas confiance à ce relativement obscur Fonction C. Puis-je prouver que la fonction ne réorganise pas les éléments égaux, pour toutes les entrées, dans mon code Idris au lieu d'utiliser un assistant de preuve distinct?

Pour faire court: non, vous ne pouvez pas. Une fonction étrangère est comme une boîte noire et le type que vous lui attribuez est une promesse que vous faites: dans la correspondance Curry-Howard qui correspondrait à l'ajout d'un axiome à votre théorie.

Cela étant dit, il existe des moyens. Dans Coq par exemple, il existe différentes formalisations de la norme C (par exemple le travail de Robbert Krebbers ). Parce que vous avez une représentation explicite des programmes C et de leur sémantique, vous pouvez écrire votre code directement dans l'assistant de preuve et il est alors possible de prouver certaines de ses propriétés.