[Avshalom]

Ada with all the runtime features left on is slower than comparable quality C. It's faster than most languages though.

With all the runtime turned GNAT can/should produce code with in a percent or two as fast as GCC (they share the same backend).

And Ada has a thing called SPARK which is a set of compiler checks to formally verify your code so you can provably turn off those runtime features safely. https://en.wikipedia.org/wiki/RavenSPARK