Keeping CALM: when distributed consistency is easy

Programming this way is already easier in a lot of places, but the boundary between non-distributed systems that are possible without mathematical thinking and the ones that can only be done with mathematical thinking is easy to ignore. It tends to be specific niches where programs are only possible with this sort of thinking, and everything else can mostly be hit hard enough with a stick until it works well enough that we can can just get on with it. But as things get distributed, it just becomes insanely difficult to build even a "correct enough" system if you're not building it with some sort of math at least held in your mind as you design it. And "distributed" isn't just about servers, it's about multi-core CPUs, it's about GPUs, it's about CPUs and GPUs, it's about networks, just everywhere you look there's more and more "distributed" arising.

I keep seeing people sell tech/languages/frameworks as some sort of replacement for deep understanding. Hey, that's cool -- as long as you don't spend all your time honking around with the tool instead of the problem. It's when these promises fail that devs and teams end up on a dark, lonely path with unhappy customers.

Overall I am quite fascinated by the concept of new environments for programmers -- and I believe it's not just new languages, but the tools, the industry background, the workflow, and a lot of other things come together to make tools and frameworks rock. (Many times we all want to geek out on language details when the problem with the language is lack of a community or tooling that makes you want to jump out a window. But I digress.)

Something I'm working on is coming up with guidelines of when and how to create good DSLs in order to create that kind of environment.

Formal methods are great in their own way but for a lot of programming tasks they overshoot the mark. For those that do not, by all means, bring them in. But right now, a practical engineer can't ignore just how klunky they are and how badly they scale up. One may gaze longingly at them, and dream fondly of the future date when they are more practical, but they aren't there yet.

There is a reason the Haskell community is always banging on about monads and monoids and applicative functors and commutivity and associativity and identifying exactly how little power you need to accomplish a given task, and it's the same reason I was able to say in another comment thread that Haskell is probably the only current semi-popular language that could deploy the ideas in this paper as a library, and that library would actually be correct. (There are some languages that could deploy the library and it would be a cultural fit, like OCaml or Clojure, but you'd still be able to trivially use it incorrectly.)

Plus even if you still want to get into formal methods and program synthesis, "learn Haskell first" is still a fairly sensible stepping stone. It probably isn't strictly mathematically true, but formal methods are going to be more-or-less a superset of what modern Haskell teaches you anyhow. Both the Haskell language and the Haskell tooling will be easier, and pragmatic enough you can do a real project like "rewrite my website in it" or other pragmatic, attainable projects that the formal methods languages can't do yet.