Differences

This shows you the differences between two versions of the page.

--- formal_methods [2022/02/05 21:12] – intro with maple domin144
+++ formal_methods [2022/02/06 14:10] (current) – domin144
@@ Line 1: / Line 1: @@
 ====== 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.
@@ Line 10: / Line 15: @@
 "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 1 = 0.
+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.
-TODO: show the sequence with sin and arc sin
+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.