9
$\begingroup$

Given that:

  1. A language with very expressive type systems (e.g. Idris) can also have escape mechanisms like foreign function interfaces/unsafePerformIO.
  2. 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.
  3. 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?

$\endgroup$
10
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.