Verus: Verified Rust for low-level systems code
1–10 of 53 posts
Re: Verus: Verified Rust for low-level systems code
#2How many of these are there?
Re: Verus: Verified Rust for low-level systems code
#3How 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.
Re: Verus: Verified Rust for low-level systems code
#4love another rust project! are there plans to expand support for concurrency primitives or async constructs in future releases?
Re: Verus: Verified Rust for low-level systems code
#5How many of these are there?
The main ones are Verus, Prusti and Creusot, but they take quite different approaches. This isn't redundant.
Re: Verus: Verified Rust for low-level systems code
#6How 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.
I think that for a guarantee as central as non-panicking, there ought to be eventually some kind of support in the core language.
(Just throwing ideas here, but there could be `#[never_panic]` for simple cases where the compiler can clearly see that panic is not possible, or error otherwise, and `#[unsafe(never_panic)]` for more involved cases, that could be proven with 3rd party tools or by reasoning by the developer like normal unsafe blocks.)
For more complicated guarantees, it's harder to see if there's enough common ground for these tools to have some kind of common ground.
Re: Verus: Verified Rust for low-level systems code
#7How 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.
I think that for a guarantee as central as non-panicking, there ought to be eventually some kind of support in the core language. (Just throwing ideas here, but there could be `#[never_panic]` for simple cases where the compiler can clearly see that panic is not possible, or error otherwise, and `#[unsafe(never_panic)]` for more involved cases, that could be proven with 3rd party tools or by reasoning by the develope…
[deleted]
Re: Verus: Verified Rust for low-level systems code
#8How 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.
I think that for a guarantee as central as non-panicking, there ought to be eventually some kind of support in the core language. (Just throwing ideas here, but there could be `#[never_panic]` for simple cases where the compiler can clearly see that panic is not possible, or error otherwise, and `#[unsafe(never_panic)]` for more involved cases, that could be proven with 3rd party tools or by reasoning by the develope…
Normal rust can already do this. For example #[no_panic] attribute is implemented in https://github.com/dtolnay/no-panic crate.
Re: Verus: Verified Rust for low-level systems code
#9Rust 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.
Re: Verus: Verified Rust for low-level systems code
#10Rust 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.
if i read it correctly, it also checks raw memory access during compilation. My assumption is that it also checks unsafe blocks, which is important when working with low level