Учитывая это:
- Язык с очень выразительными системами типов (например, Idris ) также может иметь механизмы выхода, такие как интерфейсы сторонних функций / unsafePerformIO.
- Существуют помощники по проверке, которые можно использовать для доказательства некоторых свойств программы, написанной на языке, который не имеет системы типов, способной выражать эти свойства.
- Соответствие Карри-Ховарда показывает, что успешно проверенная реализация типа функции с данным типом является доказательством того, что выражается этим типом.
Можно ли выразить нетривиальные доказательства некоторого свойства кода иностранного языка в системе типов родного языка?
Например, представьте, что у меня есть функция C с именем stable_qsort, которая сортирует числа ужасно умным и эффективным способом, сохраняя порядок уже равных элементов, и программа Idris, которая вызывает stable_qsort через свою FFI, но я не доверяю этому относительно неясному С функция. Могу ли я доказать, что функция не переупорядочивает одинаковые элементы для всех входов в моем коде Idris вместо использования отдельного помощника по проверке?