Not really. I'd place Agda or Coq above Lisp.
C if you are terrified about performance
Lisp if you are terrified about boilerplate
Agda if you are terrified about correctness
If you are terrified about all of these, then welcome to the world of engineering.
And yes, it is not used, only in some obscure and low profile projects : https://www.adacore.com/customers
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.)As it is, the static typing helps to avoid some boilerplate, too, indepedent of macros. In some sense, static typing removes, among other things, boilerplate tests.
Because more than 10 people have heard of and use Agda or Coq?
I don't think so. Last I heard, there was still a lot of COBOL out there.
Most banks, and many other businesses that have been around 30+ years, are still running on COBOL.
It was popular because of its highly readable syntax and its fixed-point packed decimal math for financial calculations.