HN Reader

Verus: Verified Rust for low-level systems code

158

How does it differ from Prusti and Creusot?

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.

9 months agoby weinzierl

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?

9 months agoby daxfohl

Previously:

https://news.ycombinator.com/item?id=32105781

https://news.ycombinator.com/item?id=36530561

https://news.ycombinator.com/item?id=35129690

https://news.ycombinator.com/item?id=40259185 (has actual discussion)

9 months agoby yencabulator

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.

9 months agoby yencabulator

How many of these are there?

9 months agoby bk496

love another rust project! are there plans to expand support for concurrency primitives or async constructs in future releases?

9 months agoby badmonster

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.

> Developers write specifications of what their code should do ... Verus statically checks ... the specifications for all possible executions of the code

This is what tests are for.

9 months agoby worldsavior