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 1 = 0.

TODO: show the sequence with sin and arc sin