To me as a programmer, to write mathematical proofs that are mechanically checked by a computer feels empowering. To have these proofs as executable programs feels even more empowering. Therefore, our proofs have a computational aspect and vice-versa: our programs have a logical aspect. To be able to get an instant feedback while proving a theorem is amazing. With Agda, a dependently typed functional programming language, one can interactively write a proof by getting guidance from Agda as to what is left to prove. Furthermore, Agda checks the correctness of proofs by following a set of rules. Unlike with pen and paper proofs, proofs in Agda are much more rigorous because there is no room for hand-waving nor unwarranted claims for something to be trivial. An uninformed mathematician will likely find this comparison to Agda hard to believe.
As announced last week, yesterday I gave a talk on function totality at the Institute of Electrical and Electronics Engineers, Croatian Section. The talk was located at the University of Zagreb at the Faculty of Electrical Engineering and Computing. Slides used during the talk are freely available. The talk was in Croatian.
Benjamin C. Pierce writes what it is like to use a proof assistant to teach programming language foundations.
Just this morning these two books landed my mailbox:
The Little Typer is a new book on dependent type theory, written by Daniel P. Friedman, an author of The Little Schemer, and David Thrane Christiansen, an Idris contributor. Verified Functional Programming in Agda is a book by Aaron Stump, on using dependent types in Agda to prove various properties of programs. After having read the Type-driven Development with Idris book by Edwin Brady, I am hoping these two books will significantly expand my knowledge of and improve my skills in type theory, theorem proving and typed functional programming. Looking forward to reading the books! If you haven’t noticed by now, I got hooked on dependent types!
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!
What is a common problem in programming is to use types that are too generic for a particular problem. If a too generic type is used, it leads to allowing values in types that don’t make any sense for the particular problem at hand, which leads to unforeseeable errors at runtime. For example, you might want to say that a particular number has to be greater than 5, i.e., x > 5. This kind of constraint is nice to have because it supports a pattern where illegal values are not representable. That way you avoid throwing exceptions at runtime when you get a value that doesn’t meet needed constraints, which allows for referential transparency, which allows for functional programming, which in turn allows for easier reasoning about your programs. In general, type systems in programming languages don’t have a way of representing a constraint like x > 5.