Near Future of Programming Languages [pdf]

I know a bit of Haskell and want to look at Idris, someday.

My point was, there should be a clean (best if even syntactic) separation between code itself (i.e. what should actually be done) and its properties (like types). Also, because there are two points of view about the properties (human and computer), this separation needs to be there twice (so for example, each type could be specified by computer and by human). I haven't seen a system that would do it, on a systematic level in the programming language. I only gave examples to show where it could be used.

For example, functions that return a different type depending on the values passed in are a useful pattern, but not allowed in staticly typed languages, except those with dependent types (Idris) or runtime downcasting (Go). There's always a way to acheive the same thing, but usually at the cost of safety or much more verbosity.

This is actually, IMHO, one way Go strikes a happy balance between static and dynamic typing. It provides a (runtime) safe and low-verbosity way to write dynamically-typed code, i.e. `interface{}`. Rust is slated to get something similar with `impl Trait` values.

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/