On Tuesday, March 26, I’ll be giving a talk on propositions as types to the Lambda Zagreb Meetup group. The talk will be in Croatian and it is titled ¬ sve za ∀ (no ∃ uvod u propozicije kao tipove), which can be translated as ¬ everything is for ∀ (but there ∃ an introduction to propositions as types). Obviously, I incorporated logic operators into the title with the goal to make it catchy and to attract more audience with an unusual title. Given that only about 10 people RSVPed so far and that there are only three days left until the talk, it looks like I’ve achieved quite the opposite!
Software testing has been an important, if not prevalent way of checking software correctness. In this article I will tell how have my doctoral dissertation on testing and verification of imperative software as well as my work experience after the studies led me to typed functional programming, which consequently gave me a different perspective on automatic software testing. Furthermore, I’ll explain why functional programming and static type systems are important for software correctness.
Philip Wadler makes a fun note about today’s programming languages: “Most of you use programming languages that are invented, and you can tell, can’t you?” I recommend watching his whole talk Propositions as Types!