Comment by LessDmesg

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.