Two quibbles: Haskell is prone to something that might be considered a class of bug that Rust avoid: the space and time performance of idiomatic Haskell code can be very surprising.
I also wonder at the possible answers you give to " “When” would you say that the software had a bug?" - the most obvious answer to me is when the commit is made to the codebase that introduces possibly observable incorrect behaviour.
My point is that I actually think that Idris could end up being successful in an industrial sense, due to the fact that it gives you all the correctness guarantees of Haskell (and more), but has managed to (thus far) avoid a lot of the cruft that has built up in the ~30 years Haskell has been around. Fingers crossed.
[1] http://docs.idris-lang.org/en/latest/reference/uniqueness-ty...
Rust's advantage is that its borrow system, with reborrowing rules and such, feels much more ergonomic.
If I knew anything about elaborate type systems, I would try and address your complaints. Sadly, my knowledge of linear logic and whatnot is very ad hoc.
The fact is that, for the vast majority of workloads, which are not heavily algorithm dependent, idiomatic Haskell is going to be much faster than what most people are using. For the algorithm dependent ones, a Haskell programmer familiar with GHC's optimization layer should suffice to get very good performance. I've written several high performance Haskell programs, and it's moderately time consuming but not anymore difficult than other languages.
I am not trying to be pedantic, but your point is moot if you consider what "most people" are using are not dynamically typed interpreted languages like Python Ruby or PHP, but rather statically typed, compiled languages like Java, C#, and C++. Java by itself dwarfs Python and Ruby combined.
Here are some benchmarks: https://github.com/jakubkulhan/hit-server-bench. As you can see, warp is on par, if not better than, many of the common JVM based options.
I'm not arguing Haskell is necessarily better than Java in all benchmarks (or C#). Merely that IME, most people dismiss Haskell as slow because it's a functional language, despite increasing evidence to the contrary. It is certainly capable of standing on its own against popular languages.
To your second point, I think the author is making an argument that it can perhaps even be earlier than that: the bug is introduced when the programmer's model of the behavior differs from reality. That is to say, the "bug" exists purely in the developer's mind. After that it's a matter of course for the bug to be transferred from there to the codebase.
If the developer chooses to interrogate their model before committing it to code, there is the possibility of the bug being caught before it ever makes it into the codebase. But perhaps it is still correct to say the bug still existed, for a short time, at least.
That is indeed one of Haskell’s drawbacks, though personally it’s one I am comfortable with given the alternatives. I’m happy for a program to be correct and less performant than fast and wrong. The performance issues are also not intractable. The tools for measuring this are pretty good.
For example, due to laziness, file-streaming with lazy IO can end up with files being closed before you're done consuming. This is almost certainly never what you want, so Haskell's system actually hurt correctness.
In that particular case it's easy to get around if you use the Conduit library, but that's just one example.
I will say that personally I have become somewhat enamored with Idris, but I think that most of the people that work on it claim that it is not production ready, and I've not used it for anything but personal projects. Still, I love that it gives me everything that I like about Haskell, and it's young enough to not have many of the drawbacks, at least not yet.