I really dislike the concept of compiler warnings. It's either an error, in which case it needs to be handled right away, or it's completely fine. Warnings are overlooked in the long run.
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.
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! :)
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.
You don’t deserve the downvotes. You need far far fewer unit tests when you have a good type system backing simply because the compiler allows you to meaningfully constrain your inputs.
Sibling comments are talking about "good types need fewer tests, yada yada" which is somewhat subjective (although I happen to agree with it).
More objectively, a dependent type system (like Idris, Coq, Agda etc.) is a test framework, since it can run arbitrary code.
Instead of writing tests as booleans, with 'true' for pass and 'false' for fail, we write them as types, with the unit type for pass ('()' in Idris) and the empty type for fail ('Void' in Idris), e.g. see this thread https://news.ycombinator.com/item?id=24567404
Of course, we can do the usual monad/effect-system tricks to implement a 'throw TestFailException' API on top of that, if we prefer.
I'll use a warning if it might be an error but I don't have enough information to be certain (most commonly when I'm trying to infer essential information about a compilation target and have a reasonable but fallible fallback for esoteric targets).
That leaves the caller of my library in control of how they want to handle such cases:
(1) If they silence warnings then everything will probably still work.
(2) If they convert warnings to errors then they can immediately inspect that warning and see how it applies to their use case. They might still just silence the warning, or they might add in some kind of override or shim so that my code works on their system.