“Our main aim is to build up a system of formal rules representing in the best possible way informal (mathematical) reasoning.” — Martin-LÃ¶f (1984, p. 4)