The goal is to support a smooth transition from ordinary programming to integrated programs and proofs whose correctness can be checked and certified by the compiler.
Scopul este de a sprijini o tranziție lină de la programele obișnuite la programele integrate și dovezile a căror corectitudine poate fi verificată și certificată de către compilator.