Really, it's not a zero-sum-game between open-source and commercial tools.
Yes, there are mathematical results that can be validated independently. But the problem is not so much pure mathematics as numerical results. In that arena, the method by which the results were acquired must be accessible in detail. And much of modern applied mathematics relies on numerical results. Imagine producing a result of some value and being unable to explain in detail how it was arrived at, because it emanated from a closed-source program.
The four-color map problem I mentioned earlier was the first important case where this problem had to be dealt with, and it was resolved to everyone's satisfaction only because the full source was made available.
Did the four-color map problem use numerical results? I imagine it was just a pure combinatorial enumeration problem (I have not read the original paper, I may be wrong about that).
If you're doing a finite element method to validate a bridge design, you're hardly publishing a paper based on the result (though of course you will do plenty of validation and then times everything by 2 for good measure!).
What kinds of actual fields of mathematics are you thinking about, here?
I know that error analysis is a deep and arcane subject, and personally I have no idea how well or badly we do in that department, but I'm struggling to think of where the details of how we get it wrong or right is crucial for the development of published academic mathematics.
"Most" maths is totally abstract these days, categories and sheaves and topi and what not.
In that case, anyone who uses more than one example to make his point is jumping around. If allowed to prevail, this non-argument would cripple debate.
> Did the four-color map problem use numerical results?
Yes, emphatically so. There were a certain finite number of possible maps (1936 to be precise), and each of them had to be tested explicitly. The reason for the requirement for full disclosure was that the tested set needed to be examined to assure that nothing germane was excluded, nothing included on specious grounds, and the manner of testing had to be closely examined. None of this could be reduced to a simple equation, and none of it yielded to a formal, concise mathematical proof.
> I imagine it was just a pure combinatorial enumeration problem (I have not read the original paper, I may be wrong about that).
If that were true, there would have been no role for a computer program -- it would have been published as a pure and formal result, like Fermat's last theorem. No one would have cared about the role played by computers, because a formal and pure proof could be examined by anyone sufficiently versed in mathematics.
> What kinds of actual fields of mathematics are you thinking about, here?
Any field that would benefit from use of a computer. By recent count, that's nearly all mathematical fields for one reason or another, including areas we once might have thought would have no use for a computer. Computer mathematics has gotten to the point where computers, laboring independently, come up with new theorems that humans have overlooked.
> I know that error analysis is a deep and arcane subject, and personally I have no idea how well or badly we do in that department, but I'm struggling to think of where the details of how we get it wrong or right is crucial for the development of published academic mathematics.
Most struggle with that, and part of the struggle is being able to see the detail of the algorithms used to arrive at a result. No detail, no trust, no science.
> "Most" maths is totally abstract these days ...
Not relevant. Relevant would be whether that abstract mathematics is or is not fully revealed in its details. For science, it must be.
This article --
http://www.newscientist.com/article/dn7286-computer-generate...
-- discusses the role of theorem-proving software like Coq, but includes a misleading statement by someone at Microsoft: "Microsoft hopes to develop a similar system for checking the logic used in computer programs, which could pre-empt some unforeseen bugs that cause programs to crash."
I hope this is an error on the part of the journalist who wrote the article, because it implies that Turing's halting problem, and Gödel's incompleteness theorems, which lie behind it, are potentially soluble. They aren't. All the more reason for full disclosure.
You don't have to _decide_ whether a program halts in order to prove it. In many cases, termination is not so much even a proof obligation as it is a _fact_ by construction; in the harder case where termination is not obvious structurally, you can simply rewrite your general recursion as a call-graph, and then termination is a proof obligation which you must satisfy if you wish to execute it.
Decidability is much a much stronger thing than "provability in most relevant cases", and it turns out that the latter suffices. By Gödel, there are indeed "true" sentences which you cannot prove in a particular system, but I am willing to give you a hundred thousand dollars if you can actually find one and print it out. That is, Gödel's result was indeed sort of constructive, in that it did provide a scheme to construct such a sentence, but nobody does so because the term is so unfeasibly large.
There are many things which we should like very much to be decidable, some of which _can_ in fact be decidable (by Turing, termination is not one of those). For instance, in some systems (such as Intensional Type Theory), type checking is decidable, which is really nice. In others, type checking is undecidable (such as in Extensional Type Theory); does this mean that type checking cannot be done? Of course not. It simply means that type checking becomes a proof obligation, since the typing derivations may not be entirely synthesized by the type checker. (A simple demonstration of this is equality in a NuPRL-like system: propositional equality is reflected into definitional equality; there is not decidable equality for functions; therefore, there are equations which might hold definitionally by equality reflection, but for which further proof would be required; therefore, definitional equality is undecidable; therefore type checking is undecidable; but we can still prove that a term is well-typed, even if type checking is undecidable.)
I do think there is a commercial side to this, too, however. This is a kind of a hook to catch future customers of the commercial package.
The sort of access to source code that is being expected here is really no more than the sort of access that you can get to Windows code. It really is not an unreasonable expectation.
I suppose that you, however, do not, which makes what I was trying to say irrelevant.