Fair enough. But even though there's no hope of coming up with a single programming language for everything, we do have quite good tools for popular areas. It seems like being able to mechanize the error-checking of proofs in certain of the more useful and popular subfields of math might be just what's needed by non-mathematicians?
Well, we do have proof assistants. I think people are starting to use those in more diverse fields of math now--I remember seeing an article about an algebraic proof in Coq, but I don't remember any of the details.
