How does it differ from Prusti and Creusot?<p>I feel, with more and more tools crowding that space, a common specification language would make sense. Sure, every tool has its own unique selling points but there is considerable overlap. For example, if all I want is to express that I expect a function not to panic, there should be one syntax that works with all tools.
Would it be better to build dependent types into the language itself so that we can guarantee any spec we want? Or do these tools have some advantage over dependent typing?
Personally, I think the verus! macro is too much in the way for this approach to be feasible. Kani or Prusti syntax is much more usable for real projects.
Rust is supposed to be a "safe" language for low level use, and thus has borrow checker, unsafe, etc. Building a "verifier" on top of Rust seems a bit excessive and unneeded.<p>> Developers write specifications of what their code should do ... Verus statically checks ... the specifications for all possible executions of the code<p>This is what tests are for.