This is a passionate plea for the proof:
Forever, in infinite many cases
A proof is the lazy brain's best friend - it prevents it from the need to test a theorem, a transformation, a change, a program…in finite many, but many!, cases. A proof says: correct in infinite many cases. From "now" on the semantics is functional not necessarily operational.
A proven theorem can be pushed into the knowledge base and used as black box. It becomes a validated building block of the innovative mathematical spiral.
Mathematical thinking
When we want to solve 3*x=5, we may be aware that rational numbers, under multiplication, (Q,*) form an Abelian group and each number is a basis for all others. To solve the equation, we use an equivalence transformation to get a basis that has nice properties for finding the solution:
3*x=5-->3/3*x=5/3-->x=5/3.
We apply the same principle if we want to solve a system of linear equations. Again, it's a helpful view to see the "unknowns" as weights for column vectors linearly combing the "goal vector".
Provided m=n and the column vectors build a basis (they are linearly independent) a unique solution exists. Again, we use equivalence transformations to get a basis with nice properties…In the matrix language it's a triangular matrix…The core of the proof is the general principle of constructing the bases.
What about a system of multi-variate polynomial equations? The Austrian mathematician Bruno Buchberger has shown that the same principle can be applied…proven by constructing the Gröbner Bases. In short, it transforms the system in a way that one basis element is only univariate.
Deep knowledge in ring theory, ideals…is required.
Algorithm generators
One of Bruno Buchberger's research project is Theorema. In short, automated theorem proving, with a system built atop Mathematica. If the Theorema software can automatically create a constructive proof for the solution of polynomial equations (by constructing Gröbner Bases) it generates the solver.
This is not required here, because GBs are already constructed. But, in general an automated theorem prover can become an algorithm generator.
Symbolic computation
The original objective of this field was
- automating mathematics (not only computation)
- empowering computer science with mathematical thinking and techniques
Remember, the term abstract data type can be regarded as a generalized approach of algebraic structures (lattices, rings, modules..), if you want it's a cousin of the "universal algebra" - a set of elements, a set of operations and a set of rules.
But, without a concrete model and implementation it remains "abstract nonsense".
What we finally want? A language to program everything? The Wolfram Language and its implementation, Mathematica, are really great, but there's still a lot to do - implementing (correctly) what can be described in the language.
There is no such thing as an abstract program. Give me constructive proofs! A Kingdom for a constructive proof!
