(Author here) it depends on your use case. If you need to incrementally acquire locks, then levels are helpful -- you can't do that with LockSets on their own. A place where this comes up is if you need to read a value out of one lock, and pick what to lock next based on that without releasing the first one, and then modify both. Of course you should think twice when doing this but when you need it, you REALLY need it.
Opting out of lock levels was a design goal. By default all locks are are Level1, so the level can be omitted thanks to the default type parameter filling it in for you. Levels have no runtime cost, so sidestepping them is free. This lets you live in an atomic-locks only world if you want, and if you later find that you need incremental locks, you can add more levels at that time :)
[EDIT: fixing autocorrect typos when I got back to my laptop]
(Author here). Early in development I did exactly this with a macro. It was confusing when you wanted to refactor the code to change lock orders, harder to make clear error messages, and so on. Forcing the user to assign in a level means that it's clear(er?) to users what's happening, we don't need fancy (and difficult to debug) macro magic, and users can still do the linearisation themselves. That's the HOPE at least.
IMO compile time locking levels should be preferred whenever possible... but the biggest problem with compile time levels is that they, well, check at compile time. If you need to make mutexes at runtime (eg mange exclusive access to documents uploaded to a server by users) then you need to be able to safely acquire those too (provided in surelock with LockSet).
Author here! This post was human written, LLM proofread, and edited a couple times as folks pointed out broken links and minor errors when it was posted to r/rust a few days ago. As someone mentioned lower in the thread, there's a form of what is sometimes called Bay Area Standard that both very online humans and LLMs have absorbed. I find it FASCINATING that we're in an era where we have to prove our humanity, and the downstream behaviours of things like killing em-dash use in response are interesting to watch in real time. I've made the same mistake, so it's honestly difficult to tell!
Author of the article here! I've actually come to agree with you since writing that article. I'm actually not a fan of mutexes in general and miss having things like TVars from my Haskell days. Just to shout out a deadlock freedom project that I'm not involved in and haven't put in production, but would like to see more exploration in this direction: https://crates.io/crates/happylock
An absolute banger of a paper! (Hellerstein is a coauthor, so immediately expected to be good). Definitely some stuff in here that's further out, but a very clear articulation (or roadmap!) of where distributed systems could go.
Verified lifting is very cool but needs lots of research, though I'm unclear that's a hard requirement for this vision to become reality.