There's a huge difference between "Verus can prove the safety of unsafe code" and "Verus can EASILY prove the safety of unsafe code." And I bet it can't prove everything, like calls to a C ABI.
Not the first time Microsoft employees invented a formal methods tool, Microsoft ignored them, and AWS scooped them up. Not the second or third time, either.
I don't think it's entirely fair to say they ignored them. As far as I know they are still employed at Microsoft Research and working on developing and improving the tool?
The key bit is that specifications don't need to be "obviously computable", so they can be a lot simpler than the code that implements them. Consider the property "if some function has a reference to a value, that value will not change unless that function explicitly changes it". It's simple enough to express, but to implement it Rust needs the borrow checker, which is a pretty heavy piece of engineering. And proving the implementation actually guarantees that property isn't easy, either!
I'll warn you that Picat is very much a "research language" and a lot of the affordances you'd expect with a polished PL just aren't there yet. There's also this really great "field notes" repo from another person who learned it: https://github.com/dsagman/picat
Side note: Just clocked your name. Read through Practical TLA+ recently modeling a few things at work. Incredibly helpful book for working through my first concrete model in practice.
- Have a clear notion of what part of the specs represents the system under your control (the "machine"), and what part represents the broader world it interacts with. The world can do more than the machine, and the properties on the world are much more serious.
- Make lots of helpers. You need them more than you think.
- Add way more comments than you normally would. Specs are for analyzing very high-level ideas, and you should be explaining your high-level ideas.
- Make the spec assumptions clear. What has to be true about the operating environment for the spec to be sensible in the first place?
- Use lots of model values, use lots of constants, use lots of ASSUME statements. Constrain your fairness clauses as narrowly as possible.
- Understand the difference between the semantics of TLA+ as an abstract notation and the semantics of TLA+ as something concretely model-checked. For example, TLA+ is untyped, but the model checker is typed. Also, a lot of TLA+ features are not available in different model checkers. OTOH, you can break TLA+ semantics with use of TLCSet and TLCGet.
The last tip applies to whatever modeling language you use: most have the same distinction.
I've had to help a client with something not exactly like, but with similar properties as, Google Docs. One of the big properties they had to engineer in was "the doc should eventually look the same for all open browser tabs on the same computer".
The other big question: what happens if user A makes change X and user B makes change Y? There's a lot of outcomes the product can pick between, but whatever they pick it should be consistent. That consistency in conflict resolution is a good property to model.
I think the "high school math" slogan is untrue and ultimately scares people away from TLA+, by making it sound like it's their fault for not understanding a tough tool. I don't think you could show an AP calculus student the equation `<>[](ENABLED <<A>>_v) => []<><<A>>_v` and have them immediately go "ah yes, I understand how that's only weak fairness"
Oh, hey -- you're that guy. I learned a lot of what I know about TLA from your writings ^_^
Consider my behavior changed. I thought the "high school math" was an encouraging way to sell it (i.e. "if you can get past the syntax and new way of thinking, the 'math' is ultimately straight forward"), but I can see your point, and how the perception would be poor when they hit that initial wall.
reply