Ada gives you neither the performance of C nor the abstraction- and boilerplate-removing power of Lisp nor the provability of Agda. This is why it is not used.

The performance is pretty close, actually (far more than Go, for example) : http://benchmarksgame.alioth.debian.org/u32/benchmark.php?te...

And yes, it is not used, only in some obscure and low profile projects : https://www.adacore.com/customers

http://benchmarksgame.alioth.debian.org/u32/benchmark.php?te... might be a better link to show how Ada performance compares to C: ranging from twice as fast to three times as slow, with a median in favor of C. It's true that it's pretty close. I don't know if those numbers are representative of how performance works out in the real world; any insights from your experience?

Golang, it's true, is in the 3×–10× ballpark.

https://github.com/languages/Ada shows Ada as the #52 most popular language on GitHub. The #10 most popular is Objective-C at 3%. Using R:

    summary(lm(log(c(25, 13, 8,8,8, 7, 6, 4, 4, 3)) ~ log(1:10)))

I derive that the Nth most popular language on Github is used in 24% * N -0.81 of projects, with an R² of 0.93. This suggests that Ada should be in use on about 0.98% of projects on Github, which makes me wonder why https://github.com/languages/Ada/updated?page=10 can only find 200 Ada projects that have been updated in the last nine months. (JS, the #1 language, has 200 projects updated in the last 22 minutes.)

That should be 24% × N ^ -0.81. The double asterisk I was using for exponentiation got eaten.

Ada. Not an acronym.