> 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?