1. In a computing environment, a system comprising, a compiler that compiles source program code written in a source language that integrates affine types with dependent and refinement types, the compiler including a type checker coupled to a solver to obtain proofs from the solver, the compiler translating the source program code into target code having the proofs associated with the target code for verifying security policies.