In my recent post The Freedom of a Financial Language I have emphasized on the benefit of a (domain specific) programming language that represents everything in symbolic expressions, for declarative programming, symbolic code manipulation, scripting ….. as a kind of freedom
When I wrote this I recalled the book Meta Math, Gregory Chaitin, about complexity, computability, randomness and incompleteness.
And think of
Computational knowledge
A little more abstractonautics: a Formal Axiomatic System is built of an Alphabet, a Grammar, Axioms, Inference Rules and a proof-checking Algorithm. Mathematical proofs must be formulated in this language and use axioms and the inference rules to create the logic "proof chain".
If the language is a an adequate programming language an automated theorem prover can create a constructive proof, a program that computes results applying the theorem.
Remember the polynomial ring. A system of multivariate polynomial equations can be solved by constructing the so called Groebner basis. The constructive proof that the Groebner bases are result of correct equivalence transformations (of the original system of polynomials) is a program that computes them. Provided, the language is a symbolic language and knows how to do the transformations.
A mathematical theorem that is proven can be pushed into the mathematical knowledge base.
A weaker, but still strong, requirement is: verified and validated. An adequate programming language helps to automate verification and validation
A a verified and validated program can be pushed into the computational knowledge base. It is a new building block for something higher. The knowledge base becomes richer and richer and higher problems can be solved easier and easier.
Freedom (the language aspect) is complemented by automation (a rich world of algorithms).
But theres is more:
Documents that are programs
In Language is too Clumsy an Instrument, I have introduced the idea of representing the cores of the term sheet in a document centered declarative (symbolic) language that comes with a vast variety of algorithms.
The vision: term sheets become documents that are computational. The same with financial reports, ...
UnRisk Financial Language is document centered, symbolic, declarative and it has built-in computational knowledge.
Enabling quants to extending it into their problem world with little code.
Announcement
This Easter weekend, Andreas Binder will introduce a nice and challenging mathematical puzzle about Goats, Wolves and Lions. For recreational maths fans and geniuses.
Picture from sehfelder
