I can't speak for op but I had a similar feeling going through the free chapters of 'Type driven development with Idris'. What blew me away was once you have such a strong type system it eliminates whole classes or errors at compile time I previously considered only checkable at runtime. Furthermore it showed that doing so allows the compiler to go from being a gatekeeper to being more of a virtual assistant that helps you write your code not just check it.
> What blew me away was once you have such a strong type system it eliminates whole classes or errors at compile time I previously considered only checkable at runtime.
Can Idris turn Haskell runtime errors into compile-time errors and, if so, which ones?
The classic one is the `head` function in idris can only be called on `Vec`s of length 1 or more. More pressingly, you can actually prove lawfulness of type classes.
Checking the head of an empty list is a simple example. (Although see https://wiki.haskell.org/Non-empty_list for an approach to avoiding these runtime errors in Haskell).
Pony language's "reference capabilities" are like this--which separates the idea of type from the access to memory, and provides another level of error-class elimination and its composition of these reference capabilities and the actor model for another reduction of runtime overhead in garbage collection (being lock-free and concurrent.)