31–40 of 53 posts
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?
It is The Dream in some ways, but it is much, much easier said than done.
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?
From glancing at https://www.andrew.cmu.edu/user/bparno/papers/verus-ghost.pd... it is more related than you think. - The various "modes" are going to be needed either way, because side-effectful functions at the type level are a research problem that probably isn't worth the effort. - The in the pure functional "promotable" fragment, it probably also makes sense to relax aliasing rules / have infinite number types /…
I think having guardrails like this is going to incredibly important as AI code gen starts taking a bigger role. Hopefully, as a separate comment mentioned, there can be a standard created so that AI tools can learn it more easily.
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.
Earlier quoted context omitted.
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.
> 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…
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
Earlier quoted context omitted.
Yes, but remember that Erlang bug discussed here last week where somebody apparently messed up SSH state transitions in such a way that people could just log in without having the password or anything? Buffer overflows etc. are absurd things that should not be possible, but preventing them is the first step towards security.
This is something that Rust should prevent, not another layer on top of Rust.
Earlier quoted context omitted.
Yes, but remember that Erlang bug discussed here last week where somebody apparently messed up SSH state transitions in such a way that people could just log in without having the password or anything? Buffer overflows etc. are absurd things that should not be possible, but preventing them is the first step towards security.
This is something that Rust should prevent, not another layer on top of Rust.
I guess you're asking why that wasn't built into Rust from the start; after all, there are programming languages with the formal verification and theorem-proving built-in, e.g. for imperative languages, the SPARK extension to Ada, as well as ATS, or for a functional one, Idris. My guess is that Rust never would have become popular if you needed to write actual formal proofs to guarantee some degree of safety, since satisfying the borrow checker is easier in comparison, and it also probably would have been a lot harder to develop Rust after that. The borrow checker simply eliminating use-after-free errors and data races in safe code was good enough.
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?
I am not aware of a viable "dependent type system". Such ones as we have are very complicated and not generally a good engineering trade off. It is The Dream in some ways, but it is much, much easier said than done.
Earlier quoted context omitted.
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)
> effect system (formerly keyword generics) Any recent link about that? Specially one that calls it effect system rather than the old name keyword generics
Earlier quoted context omitted.
Why is verification excessive but not tests? A verification of a property is stronger than a mere test of a property.
The test is supposed to be the verification.
A verification would be the equivalent of that. In practice that matters since the input space is often much larger than just one byte.
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?