If statements are boilerplate? How else would you do branching? Gotos? There are definitely cases where dependent types add a lot of boilerplate. But it's not t

If statements are boilerplate? How else would you do branching? Gotos? There are definitely cases where dependent types add a lot of boilerplate. But it's not these simple cases. And guess what. You pay for what you use. If you don't want to prove something and just run your program then you can just do it.