I just read the whole thing, the post would be even better if it includes an example for concurrency. It's not easy to imagine it just by looking at the binary search's example.
They have separate machinery for concurrent code: <a href="https://verus-lang.github.io/verus/state_machines/intro.html" rel="nofollow">https://verus-lang.github.io/verus/state_machines/intro.html
m00dy · · focus · HN ↗
gregwebs · · focus · HN ↗