Personal site of Dominik Wójt

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
====== Formal methods ======
{{indexmenu_n>20}}

===== My pursue for math in computers =====

==== Discovery of computer algebra systems ====

My fascination with formal methods started, before I knew there is such thing and how it is called.

At my 3rd year of academic studies a took a course on computer algebra systems.
The system which was explored during the course was Maple.
It was really nice to see a system, in which you could convey your derivations.
It did take over a lot of tedious computations.

"No more silly mistakes or silent assumptions. All the derivations will be now correct and complete!" I thought to myself.

The euphoria did not last long. Soon, I realized, that Maple actually does a lot of silent assumptions.
I found a three step sequence to make Maple admit that ''2 π = 0''.

I have no access to maple right now to reproduce the case, but it involved combining ''g(f(x))'', where ''f(x) := sin(x)'', ''g(x) := asin(x)''.
Maple would happily compute: ''h(2*π) = 2*π''.

I am not sure, if current version of Maple would do the same. Later I found an example on the web, in which maple was cheated in just one step. I cannot find it right now. Anyway, it shows, that Maple, like all the other [[computer algebra systems]] I checked, does not follow strict mathematics.

==== Brute force attempt ====

Unsatisfied with the [[computer algebra systems]], I tried to write a simple "calculator" on my own.
Numerous problems appeared.
How to e.g. represent a generic subset of real numbers?
One could try to represent it a sum of ranges.
This would not cover e.g. set of rational numbers.
Even a set of even numbers would have an infinite representation.

The conclusion is: to have a generic representation for mathematical objects, one has to keep it's symbolic definition, just like one writes it in ones paper notebook!

As with any idea, which is good and simple, someone had to find it before me.
A new search through the web started. This time term "symbolic computation".
Still, not exactly what I wanted.

==== Metamath ====

Somebody must have defined strict rule to operate on the symbols.
After making another search, I finally hit [[http://us.metamath.org/|Metamath]] and it's companion the Metamath book.

Reading the introduction was enlightening.
All mathematics reduced to few axioms, inference rules and the rewrite principle.
This was my first encounter of axiomatic approach, set theory, etc.
I think, the first chapter of this book is a must read for every mathematician or engineer.

Now, what was needed was a [[computer algebra systems|computer algebra system]], which would produce, apart from the result, a proof of the results correctness.
I started with a simple exercise, just to get hang of the new subject.
I wrote a [[https://github.com/domin144/metamath_playground|parser and verifier for the metamath language]].

==== More formal methods ====

As one would expect, I soon got tired of this work.
I started to look further for existing solutions.
The interesting sources I found are [[http://www.cs.ru.nl/F.Wiedijk/|Freek Wiedijk's page]] and [[Coq]].

Here I am now, studying the formal methods and collecting my findings on this page.