4 ms·

> This has nothing to do with threading Right, but all the promises of the type system have to lead to a first-class multi-threading experience at some point.

• vlovich123 2y ago
  It doesn’t automatically solve every possible problem for you just like something like Lean doesn’t prevent you from writing buggy proofs. I’d argue it does lead to a first-class multi-threading experience within the systems programming domain it’s targeting. Even outside systems programming it can be quite surprisingly good and most incorrect code fails to compile to begin with. Is there a language that in your opinion offers a better multi-threading experience?
  • mrkeen 2y ago
    I think 70's style ACID-ish transactions are the way to go. Single-threaded reasoning safely transfers across to multi-threaded situations. Parent mentioned them above, argued that that ownership supersedes them, >>> Clojure has software transactional memory. With ownership it wouldn't need half of the machinery (only that for rollback) but then only showed a single-threaded demo of ownership. I don't need STM either if I'm only on a single thread. STM's a good model. You just write code as if it were single-threaded, slap an 'atomically' around the lines which shouldn't be logically divisible, and you're basically done.
    • j-pb 2y ago
      I'm not sure how to make the multithreaded case more explicit. The point is that with ownership the multi-threaded case does look exactly like the single threaded case, just with some machinery to "aquire" all the things you want to own snd do the transaction over. But "aquiring" them just looks like having them all in local scope, so there is no explicit `lock`. In the transactional case you mentioned there can still be multiple transactions having access to the same values, so you need the explicit transaction semantics. Ownership never has such cases, unless you use locks to manage ownership between threads, but it could also be done via channels, or CSP, or whatever.