Actually, there are binary numbers in the coq standard library. N is in the library NArith and Z is in the library ZArith. Both are binary.

Coq is not meant to be a language for computation. If you only use natural numbers to state properties like forall a b: nat, a + b = b + a there is nothing to unfold about them and no need to worry about inefficient computation.

There is an obvious equivalence between unary numbers and binary numbers. Should be quite easy to support inductive proofs with unary numbers while supporting computation with binary numbers, and simply translate between them depending on what context one is in. In fact, I believe this is what Coq does behind the scenes.

Unary numbers have a nice inductive definition with a base case, which makes them very easy to use for proofs. And as they are used heavily in the foundations of math they will be present when you are implementing any current fields in math. And you can always convert them to binary numbers at runtime if you want performance.

It's not about performance. Unary numbers are extremely cumbersome and confusing for proofs, because people are used to working with integers using arithmetic, not pattern matching. "x + 5" is infinitely better than "Succ(Succ(Succ(Succ(Succ(x)))))“. I suspect that dependently-typed languages will get at least a 50% boost in mindshare once they ditch the unary and rewrite the tutorials with regular numbers.

Please look at the OP. Notice the arithmetic expressions such as "Compute 3 + 4.", which returns "7 : nat" instead of a string of Succ applications to some Zero.

You're arguing against a problem that doesn't exist. Coq is fully capable of understanding decimal arithmetic. The fact that it uses a unary representation in proofs is not a burden that the user has to bear. (It's still a property that they can exploit of course, e.g. in inductive proofs.)

Have you actually done any proofs in one of these systems? (or used one?)

Natural numbers are used because of the induction principle you get: it's very useful, and generally straightforward to use in lots of contexts (e.g., just the other day I had students proving the correctness of multiplication implemented as iterated addition; the multiplication is over integers, but the inner loop is after you've ensured what you are iterating is non-negative, since you decrement each iteration, and _proving_ it is much more straightforward if you interpret the loop counter as a natural number).

And your point about syntax is also baffling: Coq will display natural numbers as decimal literals, not "S(S(S...".

>Unary numbers are extremely cumbersome and confusing for proofs, because people are used to working with integers using arithmetic, not pattern matching. "x + 5" is infinitely better than "Succ(Succ(Succ(Succ(Succ(x)))))“.

Have you ever written a proof using decimal numbers? Unary numbers (Peano numbers) only have two cases to match on: Z and Succ. Decimal numbers have at least ten. Even writing proofs for binary numbers in Coq is much more cumbersome than proving things about unary numbers.