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