Type systems and proofs

Today at KIKA Hackerspace we had an interesting event related to proofs and type systems.

We started with Coq syntax for inductive types, definitions and fixpoints. Then proceeded by defining natural numbers in Coq along with arithmetic.

So far so good, we can do the same stuff with TypeScript and most other typed programming languages.

Then we watched Idris: type safe printf which was an interesting introduction to how Idris supports dependent types.

Going back to Coq, we proceeded by defining product type pair and shown the Curry-Howard correspondence (types are theorems, programs are proofs) between swap and commutative AND.

We took a look at tactics and how they can generate lambda abstractions and applications based on some automation.

Entering the dependent types realm, this is where languages like TypeScript are limited in a sense, since you cannot make a type based on some values (note it is different to make a type based on some type).

Dependent types allow for some interesting stuff like proving specific propositions where propositions are types (e.g. forall x : X, x > 2 -> x > 1), but they also allow forall itself to be defined in terms of them. The reason most IO languages don’t support them is because of the undecidability problem.

The take away was that, depending on the abstraction level we are working, types and proofs can give us a sense of safety based on some truths we take for granted (axioms), and this is how we program everyday. We have an initial base we trust and from there we start building our abstractions.

However, this is not always easy to achieve. E.g. consider we have a button that is supposed to download a PDF. In order to prove that, you first pick the abstraction level and then proceed by defining things (what is a PDF, what is a download).

Bonus: Since it seems that Idris supports both IO and dependent types, we discussed some interesting and weird cases such as, what happens if you compile a program which types depend on some SQL database, and then after a while the schema changes. We would still have to handle stuff at runtime if we were to run an old executable.