What's the point of dependent types?

There are many languages for telling computers what to do. In some languages, you have to tell the computer what kind of things it can use to do something. Often this is good, like when stopping the computer from confusing numbers with words.

In most languages you can say simple things like “this is a number” or “this is a group of words”. The computer will check that what you say is true before it does anything.

In some languages, you can say much more. You can say things like “this is a number and it is bigger than zero” or “if this thing a group of words, then this other thing must be a group of words with an extra word”. Again the computer will check this. This means you can better prove that computer will do what you think it should do.

This is good, because this way you can be sure that computer does what you want. The problem is that so far it is hard work to make the computer understand what you want. Only people who have trained a lot can do it.

This was an attempt to briefly explain the point of dependently typed programming languages using only the 1000 most common English words (according to Cleartext).

Comments or questions? Send me an e-mail.