Can a type system serve as a proof assistant for foreign functions?

Given that:

• A language with very expressive type systems (e.g. Idris) can also have escape mechanisms like foreign function interfaces/unsafePerformIO.

• There are proof assistants that can be used to prove some properties of a program written in a language that doesn't have a type system capable of expressing those properties.

• The Curry–Howard correspondence shows that a successfully type-checked implementation of a function with a given type is proof of what is expressed by that type.

Can one express non-trivial proofs of some property of foreign language code in the type system of the native language?

For example, pretend I have a C function called stable_qsort that sorts numbers in a terribly clever and efficient way while maintaining the order of already equal elements, and an Idris program that calls stable_qsort via its FFI, but I don't trust this relatively obscure C function. Could I prove that the function doesn't reorder equal elements, for all inputs, in my Idris code instead of using a separate proof assistant?

Long story short: no you can't. A foreign function is like a black box and the type you ascribe to it is a promise you make: in the Curry-Howard correspondence that would correspond to adding an axiom to your theory.

That being said, there are ways. In Coq for instance, there are various formalisations of the C standard (e.g. Robbert Krebbers' work). Because you have an explicit representation of C programs and their semantics, you can write your code directly in the proof assistant and it is then possible to prove some of its properties.

StackExchange Computer Science Q#71074, answer score: 10