EDIT: I originally meant this as a joke, but seriously, if someone accurately knows where the gotchas are, that's valuable. Also note if they're biased to false positives and/or false negatives, and by how much. Are their heuristics for dealing with unknown territory efficient and likely to converge on good approximate results?

I'm terrified by what I don't know, especially by what I don't know that I think I should know, to be "in the know".

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.

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.

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)))

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.