I think they're better largely because I'm more aesthetically drawn to them (so I will be biased, but no more so than the author, who also only mentions techniques he's aesthetically drawn to), but also because I think they have shown more success in practical industry use.
For programming interactive systems, a very interesting approach which has been quite successful in realtime software and hardware systems, is synchronous programming[1]. It has a deep mathematical theory based on temporal logic, and has been shown successful both in terms of being amenable to particularly powerful forms of formal verification[2], as well as being useful for socially managing the development process[3]. The approach has mostly remained in the realm of safety-critical realtime, but has started making its way to "ordinary" software in languages such as Céu[4] and Eve[5]. Eve, in particular, incorporates at least as much cutting-edge PL research as Idris, but is very different from it, being based on a new and interesting language semantics called Dedalus[6].
In synchronous programming, side effects are not an issue, as the mathematical framework cleanly treats them the same as computation (not requiring embedding in monads), and so allows easy specification over both computation and effects, and a particularly easy way to express global correctness properties (e.g. [7]). The use of monads/algebraic effects in pure-FP is not substantially different from classical imperative programming, other than restricting the effect type, which doesn't seem to me to yield any substantial benefits in general. Using what is perhaps a very bad analogy, given the task of counting the number of passengers on a moving train, classical imperative programming would correspond to a person standing outside the train with a pair of binoculars, pure-FP would be like someone filming the train and then studying the film, and SP would be like someone standing inside the train. Rather than controlling what effects can be emitted by a piece of code, it controls at which point the passage of time can be observed.
In terms of formal methods, TLA+ [8] (a personal favorite of mine) has proven to be very effective, both in theory as well as industry practice -- perhaps more so than any other formal tool -- especially when it comes to specifying and verifying global correctness properties, such as "the database is always consistent", or "data is never lost, even if messages are dropped and nodes fail". It, too, is based on temporal logic, which is a theory that is much better suited, IMO, to interactive/concurrent/distributed software than the theory pure-FP, which is more harmonious with sequential, batch software like compilers. The difference in the difficulty of use of TLA+ vs a tool like Lean [13] for the purpose of software specification and verification (as opposed to doing formal "high math") is the difference between riding a bicycle and flying a Boeing 747.
As far as code-level formal methods are concerned, I find contract systems (like JML [9] for Java, and ACSL [10] for C/C++) to be more promising, again, in my personal opinion, than dependent types, because they separate specification from verification. This is important because while specification is always helpful, the chosen form of verification can make the whole difference between something that's more effective than testing and something that's completely infeasible. The most rigorous form of verification is formal proof, which is both the level of confidence least required by software and more or less the only form of verification afforded by dependent types, at least today. In contrast, contract systems allow you to verify your specification at a level of rigor of your choosing -- even on a per-contract basis -- be it formal proof, model checking or static analysis, concolic testing [11], random test generation [12], or even just inspection.
Eve looks interesting, thanks I'll try it out. (And the detailed response.)
Most of my programming is in the domain of "take some data, do stuff to it, produce an output" and my experience with Idris so far is very positive -- more so than Haskell (which I admittedly gave up on early on), the language does feel ergonomic, and like the type system is "guiding me" rather than getting in the way. I also find its approach to metaprogramming interesting. Whether this translates to Real World™ productivity / maintainability gains vs a mainstream language, it's too early for me to compare.
BTW, to get a sense of how meticulous Eve's design process is (although I don't know if they'll ultimately be successful in their goal), take a look at this short post, explaining how they've recently decided to change the Eve UI after writing Eve's compiler in Eve (in the previous iteration it was written in Rust): https://groups.google.com/forum/#!msg/eve-talk/tLgrw4zlc5U/V...
I don't doubt that Idris is a fine language or that some people will love it, even though personally I'm not drawn to pure-FP; I do doubt its revolutionary bottom-line impact.
For programming interactive systems, a very interesting approach which has been quite successful in realtime software and hardware systems, is synchronous programming[1]. It has a deep mathematical theory based on temporal logic, and has been shown successful both in terms of being amenable to particularly powerful forms of formal verification[2], as well as being useful for socially managing the development process[3]. The approach has mostly remained in the realm of safety-critical realtime, but has started making its way to "ordinary" software in languages such as Céu[4] and Eve[5]. Eve, in particular, incorporates at least as much cutting-edge PL research as Idris, but is very different from it, being based on a new and interesting language semantics called Dedalus[6].
In synchronous programming, side effects are not an issue, as the mathematical framework cleanly treats them the same as computation (not requiring embedding in monads), and so allows easy specification over both computation and effects, and a particularly easy way to express global correctness properties (e.g. [7]). The use of monads/algebraic effects in pure-FP is not substantially different from classical imperative programming, other than restricting the effect type, which doesn't seem to me to yield any substantial benefits in general. Using what is perhaps a very bad analogy, given the task of counting the number of passengers on a moving train, classical imperative programming would correspond to a person standing outside the train with a pair of binoculars, pure-FP would be like someone filming the train and then studying the film, and SP would be like someone standing inside the train. Rather than controlling what effects can be emitted by a piece of code, it controls at which point the passage of time can be observed.
In terms of formal methods, TLA+ [8] (a personal favorite of mine) has proven to be very effective, both in theory as well as industry practice -- perhaps more so than any other formal tool -- especially when it comes to specifying and verifying global correctness properties, such as "the database is always consistent", or "data is never lost, even if messages are dropped and nodes fail". It, too, is based on temporal logic, which is a theory that is much better suited, IMO, to interactive/concurrent/distributed software than the theory pure-FP, which is more harmonious with sequential, batch software like compilers. The difference in the difficulty of use of TLA+ vs a tool like Lean [13] for the purpose of software specification and verification (as opposed to doing formal "high math") is the difference between riding a bicycle and flying a Boeing 747.
As far as code-level formal methods are concerned, I find contract systems (like JML [9] for Java, and ACSL [10] for C/C++) to be more promising, again, in my personal opinion, than dependent types, because they separate specification from verification. This is important because while specification is always helpful, the chosen form of verification can make the whole difference between something that's more effective than testing and something that's completely infeasible. The most rigorous form of verification is formal proof, which is both the level of confidence least required by software and more or less the only form of verification afforded by dependent types, at least today. In contrast, contract systems allow you to verify your specification at a level of rigor of your choosing -- even on a per-contract basis -- be it formal proof, model checking or static analysis, concolic testing [11], random test generation [12], or even just inspection.
[1]: https://en.wikipedia.org/wiki/Synchronous_programming_langua...
[2]: https://en.wikipedia.org/wiki/Esterel
[3]: http://www.wisdom.weizmann.ac.il/~harel/papers/Statecharts.H...
[4]: http://www.ceu-lang.org/
[5]: http://witheve.com/philosophy/
[6]: https://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-...
[7]: http://witheve.com/philosophy/#correct
[8]: https://lamport.azurewebsites.net/tla/tla.html
[9]: http://www.openjml.org/
[10]: https://frama-c.com/acsl.html
[11]: https://en.wikipedia.org/wiki/Concolic_testing
[12]: https://clojure.org/guides/spec#_testing
[13]: https://leanprover.github.io/