4 ms·

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

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.

GolDDranks 2y ago
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.
- deleted 2y ago
  [deleted]
- noxer 2y ago
  Normal rust can already do this. For example #[no_panic] attribute is implemented in https://github.com/dtolnay/no-panic https://github.com/dtolnay/no-panic crate.
  - GolDDranks 2y ago
    Via an unreliable, linker-based hack.
    - rowanG077 2y ago
      On one hand you are right. On the other hand knowing it can't panic because the code is literally not there is a very strong guarantee.
- hmry 2y ago
  I think the current plan is to integrate never-panic into the upcoming effect system (formerly keyword generics), along with const and async. So all these function annotations can share the same behavior and syntax, and higher order functions can be generic over them (e.g. "iterator.map(f) is never-panic if f is never-panic" etc)
  - nextaccountic 2y ago
    > effect system (formerly keyword generics) Any recent link about that? Specially one that calls it effect system rather than the old name keyword generics
    - NobodyNada 2y ago
      Here's a semi-recent link (~a year ago) by one of the leaders of this initiative: https://blog.yoshuawuyts.com/extending-rusts-effect-system/ https://blog.yoshuawuyts.com/extending-rusts-effect-system/
giltho 2y ago
A common specification language is a very ongoing discussion, we just haven't managed to find an agreement yet. Things like `#[no_panic]` make sense, but it also doesn't require a spec language at all, the compiler already has support for these kinds of annotation and anyone could catch it. Though I cannot think of a single verification use case where all I want to check is the absence of panic.
- nicce 2y ago
  > single verification use case where all I want to check is the absence of panic. Basically any decoder/deserializer. It might be sufficient to handle the correctness in tests but panics are the most severe thing you want to avoid. How well `#[no_panic]` actually works in practice? There might be cases where e.g. index access violation never happen but compiler might still think that it happes. I could be impossible to restructure code without adding some performance overhead.
  - freeone3000 2y ago
    #[no_panic] has false-positives, but no false-negatives. If it’s present, the code won’t panic and can’t panic. Index access violation that “never happens” is the root of every buffer overflow, so I’m absolutely OK with the minimal overhead behind the bounds check for actual safety
- littlestymaar 2y ago
  > Though I cannot think of a single verification use case where all I want to check is the absence of panic. Not for verification but in terms of ease of use, having no panic in a program means it would be fine and safe to have pointers to uninitialized memory (it's currently not because panics means your destructors can be run anywhere in the code, so everything must be initialized at all time in safe rust).
- imtringued 2y ago
  One more case where the halting problem adds more confusion than it helps. The halting problem is equivalent to the acceptance problem, which is equivalent to the reachability problem. >Though I cannot think of a single verification use case where all I want to check is the absence of panic. You can reduce any static verification task to a check for a condition that produces a panic. In short, sprinkle your pre, post and intermediate conditions all over your code in a way that produces a panic (known as asserts) and the tool will do the heavy lifting.
deleted 2y ago
[deleted]
meling 2y ago
See the related work section in the SOSP 2024 paper. I think verification speed is one of the main benefits of verus. https://www.andrew.cmu.edu/user/bparno/papers/verus-sys.pdf https://www.andrew.cmu.edu/user/bparno/papers/verus-sys.pdf

GolDDranks 2y ago

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.

deleted 2y ago
[deleted]
noxer 2y ago
Normal rust can already do this. For example #[no_panic] attribute is implemented in https://github.com/dtolnay/no-panic https://github.com/dtolnay/no-panic crate.
- GolDDranks 2y ago
  Via an unreliable, linker-based hack.
  - rowanG077 2y ago
    On one hand you are right. On the other hand knowing it can't panic because the code is literally not there is a very strong guarantee.
hmry 2y ago
I think the current plan is to integrate never-panic into the upcoming effect system (formerly keyword generics), along with const and async. So all these function annotations can share the same behavior and syntax, and higher order functions can be generic over them (e.g. "iterator.map(f) is never-panic if f is never-panic" etc)
- nextaccountic 2y ago
  > effect system (formerly keyword generics) Any recent link about that? Specially one that calls it effect system rather than the old name keyword generics
  - NobodyNada 2y ago
    Here's a semi-recent link (~a year ago) by one of the leaders of this initiative: https://blog.yoshuawuyts.com/extending-rusts-effect-system/ https://blog.yoshuawuyts.com/extending-rusts-effect-system/

giltho 2y ago

A common specification language is a very ongoing discussion, we just haven't managed to find an agreement yet. Things like `#[no_panic]` make sense, but it also doesn't require a spec language at all, the compiler already has support for these kinds of annotation and anyone could catch it. Though I cannot think of a single verification use case where all I want to check is the absence of panic.

nicce 2y ago
> single verification use case where all I want to check is the absence of panic. Basically any decoder/deserializer. It might be sufficient to handle the correctness in tests but panics are the most severe thing you want to avoid. How well `#[no_panic]` actually works in practice? There might be cases where e.g. index access violation never happen but compiler might still think that it happes. I could be impossible to restructure code without adding some performance overhead.
- freeone3000 2y ago
  #[no_panic] has false-positives, but no false-negatives. If it’s present, the code won’t panic and can’t panic. Index access violation that “never happens” is the root of every buffer overflow, so I’m absolutely OK with the minimal overhead behind the bounds check for actual safety
littlestymaar 2y ago
> Though I cannot think of a single verification use case where all I want to check is the absence of panic. Not for verification but in terms of ease of use, having no panic in a program means it would be fine and safe to have pointers to uninitialized memory (it's currently not because panics means your destructors can be run anywhere in the code, so everything must be initialized at all time in safe rust).
imtringued 2y ago
One more case where the halting problem adds more confusion than it helps. The halting problem is equivalent to the acceptance problem, which is equivalent to the reachability problem. >Though I cannot think of a single verification use case where all I want to check is the absence of panic. You can reduce any static verification task to a check for a condition that produces a panic. In short, sprinkle your pre, post and intermediate conditions all over your code in a way that produces a panic (known as asserts) and the tool will do the heavy lifting.

deleted 2y ago

[deleted]

meling 2y ago

See the related work section in the SOSP 2024 paper. I think verification speed is one of the main benefits of verus. https://www.andrew.cmu.edu/user/bparno/papers/verus-sys.pdf https://www.andrew.cmu.edu/user/bparno/papers/verus-sys.pdf