[eek04_]

I really want to love types. But type errors so so get in the way of getting to something testable - it's all "satisfy the compiler" which either requires writing out close to my whole program or writing a lot of temporary lies.

I used to program with annotated type languages (Pascal, C++, Java) for a couple of decades. I spent a decade plus with dynamically checked languages, and whenever I try to go back (to Java or C++) or go to something harder (e.g. Haskell) the type checking is very much in the way of initial development. Maybe dependent types are sufficiently expressive that this problem isn't there. However, every time the promise has been made in the past, it's turned out (IMO) that the person advocating is used to working around the weaknesses of strongly typed languages and neither is used to exploiting the strengths of dynamically checked languages nor is used to working around the weaknesses of dynamically checked languages.

[ArchieMaclean]

Idris has 'holes', where you tell the compiler that you haven't written this part yet, and it will compile while ignoring the hole.

They're really useful for rapid prototyping, and also for helping you develop, as you can ask the compiler questions about the hole (like what its type is).

The syntax is just `?name` creating a hole called 'name'.

So you don't have to write the whole program, and you don't need to lie temporarily either! :)

[chongli]

it's all "satisfy the compiler"

That’s not at all like the experience programming with Idris. Idris is more like working with a powerful assistant that can infer all kinds of stuff about the shape of your function. In some cases, it can even infer the entire function implementation from the type. In cases where it can’t infer that it can give you a bunch of information about what terms are in scope with the appropriate types.