If you wrote an S-Expression syntax on top of Agda (or Haskell), you gain all of Lisps anti-boilerplatitude for free. There's of course also Template Haskell.

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.

If you are terrified about all these, there is ADA.

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.