3 ms·

That is because mathematics tolerates informal proofs. Try to do formal mathematics (Coq, Agda, Isabelle/HOL, etc) and you will immediately see that it is not t

That is because mathematics tolerates informal proofs. Try to do formal mathematics (Coq, Agda, Isabelle/HOL, etc) and you will immediately see that it is not the case that {{a,1},{b,2}} = {{a},{a,b}}. Different definitions of "the same thing" are not "equal" but "isomorphic", and the isomorphisms are a bureaucracy that cannot be ignored -- unless you are doing regular, that is informal, mathematics and all this isomorphism business is just too tedious and 'obvious'. 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.

gnulinux 8y ago
> you will immediately see that it is not the case that {{a,1},{b,2}} = {{a},{a,b}}. 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.