Maybe add a section to discuss FFI? #20
Description
Declaring an FFI function is just declaring an unsafe wrapper that simply cast arguments and result when calling the unsafe function of the other language. The proof of that unsafe call can either use the wrapper pre-condition (thus the wrapper is unsafe) or not (the wrapper is safe).