Ada/SPARK is a strong typed C with visibility done correctly. (you know the "private" notion in C++ ... and sane scoping using semantic grade packages) All checks in Ada/SPARK can be removed so essentially you end up, in production, with code as performant as C.