In this section, I will be occasionally sharing some programming related write-ups.
In this write-up I will share the story, ideas, progress, and in particular my contribution to development of our framework for automated testing of Smart ID Desktop App we are developing in Nexus. In broader sense, I speak about testing of UWP applications, which our app is an example of.
In 2019 I decided to learn a bit about automated proof verification which in fact is a growing field in mathematics that attempts to
eliminate human errors while writing/reading proofs,
create database (encyclopedia) of mathematical results, and
do the two thing above in a human friendly form.
After some investigation we (I and my bachelor student Jáchym Šimon) decided for a rather recent, open-source, and dynamically progressing proof assistant Lean (developed at Microsoft Research) to formalize completeness theorem of classical.