goto, the marvelous

IT folks are prone to prejudices, as we all are. Once a beginner programmer starts exploring the world of coding, he quickly learns catchy memes from the more experienced part of the community. One can then easily live by them without putting much thought in their meaning.

Proving dependent equalities in Coq with SSReflect

Proving dependent equalities in Coq is boring, but quite frequently done.

Causation in modern philosophy of science

Our minds use the notions of cause and consequences all the time. It is, without a doubt, one of the fundamentals of human reasoning. However, when observed closely and formally, it becomes apparent that our concept is based rather on intuition and lacks strictness and connection to the real word. This post is intended as a quick introduction to causation from the philosophical point of view.

How to prove certain type inequalities in Coq

Sometimes you just want to prove that nasty ~ T = U for some types T and U. Well, while in general it is not decidable (nor provable), sometimes there is a relatively easy way to do it, when T and U are not both infinite. In other words, either T or U, or both of them should be finite.