1. A system comprising: at least one processor; and a memory communicatively coupled to the at least one processor; and one or more software components stored on the memory comprising: a compiler component to compile source program code written in a source language that integrates affine types with dependent types and refinement types, wherein the compiler component further includes a type checker component coupled to a solver component to obtain proofs of refinement formulas from the solver component, wherein the compiler component further to: translate the source program code into target code having the proofs associated with the target code, verify security policies, and translate each value of a refinement type within the source program into a proof term of a corresponding refinement formula.