We propose a secure compilation chain for statically verified partial programs with IO. The source language is a subset of F* in which one can write and statically verify a partial IO program that interacts with its context via a strongly-typed higher-order interface, which includes refinement types as well as pre- and post-conditions that can talk about past IO events. The target language is a subset of the source in which the compiled program can be securely linked with a context via a weakly-typed interface, without refinement types or pre- and post-conditions. Compilation converts the logical assumptions the program makes about the context to runtime checks, while linking instruments the context by adding a reference monitor to soundly enforce a global safety property. In addition to soundness, we proved in F* that our secure compilation chain satisfies by construction Robust Relational Hyperproperty Preservation, which is the strongest secure compilation criterion of Abate et al. (CSF’19).