[bmitc]

> One reason it matters to me is that if I write a program that computes something in a proof, I need to be able to understand and verify (or possibly check that other people I trust have verified) the source and algorithms

Do you actually do this verification? How do you accomplish this? The software stacks are huge. Why do you trust other people over the people who develop Mathematica, who just happened to be paid?

[mixedmath]

Yes, I do. And open source software can have papers and algorithms documenting various aspects. This is very much like using results of other math research papers, in that there is communal review and trees of dependencies and everything can be cross-verified.

It is also true that, just like with a generic math research paper, that I don't check every claim of every step of every implementation of every algorithm in the process. But checking is possible, and when we find errors (which we do frequently) we can look and try to explain what it happening.

But when we find errors in tools such as Mathematica, we cannot. We report the errors and then know nothing more. (And sometimes the errors are never fixed).