The problem with programming is that it is always fully formal. It may be lacking in rigour, but it is formal nevertheless. A compiler cannot process informal code (syntactically or semantically) and there is nothing it can classify as "obvious". Hence you need to spell everything out.
Mathematics is like programming in pseudocode, that's why it's so neat.
This is true for the examples you gave i.e. Agda and Coq but this is not a theoretical restriction. As long as you can formalize equality with something like axiom of univalence, you can prove similar things (e.g. forall x, f(x) = g(x) => f=g which gives interesting applications like mergeSort = quickSort). Proving univalence constructively is pretty hard, but it's at least partially solved, e.g. cubic type theory can constructively prove univalence. Agda has a branch that has cubic type theory implemented, if you want to check it out. There is also an "official" implementation of cubic type theory by the team who wrote the original paper but it's a pretty lean programming language without even unification.
For example, there's multiple formal definitions of integrals. They aren't strictly equivalent! But when we calculate an integral, we don't concern ourselves with the differences unless they are relevant.
Once you define something in mathematics, how you defined it does not matter. You can forget all irrelevant details. In the software irrelevant minute details make systems incompatible.
As an example, Norbert Wiener defined ordered pair as:
Hausdorff defined it as: Kuratowski's definition .. and there are many other definitions and variations, but still we have only one mathematics not many incompatible ones. Some mathematicians restrict them to subsets, but they don't create incompatible mathematics.If you do something similar in programming languages, you get two different structures you can't use interchangeably without transformation (it incompatibility starts from little endian vs big endian and ending ends with vi vs emacs).