Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Verus: Verified Rust for low-level systems code

github.com

Post reply on HN
Print view View original

41–50 of 53 posts

Re: Verus: Verified Rust for low-level systems code

#41

Post by jerf »

Ericson2314 wrote: post #37
jerf wrote: post #31

Earlier quoted context omitted.

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.

We've head them for 20 years. Lean is getting a lot of attention. Dependent types are not very complicate --- proofs are very complicated, but that is inherent. Dependent types are "only pay for what you prove" --- if you don't try to prove anything there is no problem.

I'll cop to the word "viable" doing a lot of heavy lifting there, but I have not yet seen a dependent typing system that is adequate for engineering work. There are research systems, yes, and there are many people doing laudable work on it, but when people on HN pine for "dependent type systems", I think they're talking about wanting to live in a world where most people who are programming today are instead programming in dependently-typed systems happily and productively, not a world where all programmers not functioning at a PhD-candidate level are evicted from the profession because they can't handle proof languages.

Or, to put it another way, there is no dependently-typed language I can even consider saying to my manager "Hey, you asked me to do X and I think I'll use language Y which is dependently typed", and as far as I can see, the problem isn't just that "nobody has built the standard library for it yet" or any thing else, the problem boils down to, they just aren't easy enough to use to call them practical.

I'd also say that "hey, you can use this dependently-typed language, just don't try to actually use the dependently-typed features" is also not what people are pining for.

Re: Verus: Verified Rust for low-level systems code

#42

Post by zozbot234 »

Ericson2314 wrote: post #37
jerf wrote: post #31

Earlier quoted context omitted.

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.

We've head them for 20 years. Lean is getting a lot of attention. Dependent types are not very complicate --- proofs are very complicated, but that is inherent. Dependent types are "only pay for what you prove" --- if you don't try to prove anything there is no problem.

> Dependent types are "only pay for what you prove" --- if you don't try to prove anything there is no problem.

I have to disagree with this, since fully general dependent types seem to inherently involve a kind of compile-time evaluation. You can recover a sort of phase distinction (i.e. a post-compile "run time" phase) but only AIUI through an "extraction" step that dispenses with the actual dependently typed parts of the program.

Re: Verus: Verified Rust for low-level systems code

#43

Post by meling »

weinzierl wrote: post #3

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.

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

Re: Verus: Verified Rust for low-level systems code

#44

Post by worldsavior »

GolDDranks wrote: post #27
worldsavior wrote: post #22

Earlier quoted context omitted.

The test is supposed to be the verification.

Test verify that the code works on specific inputs. Formal verification checks that it works on every input.

Can't you make the tests check every input? (This is also what they're supposed to do.)

Re: Verus: Verified Rust for low-level systems code

#45

Post by sangel »

worldsavior wrote: post #44
GolDDranks wrote: post #27

Earlier quoted context omitted.

Test verify that the code works on specific inputs. Formal verification checks that it works on every input.

Can't you make the tests check every input? (This is also what they're supposed to do.)

Obviously not. Suppose the input to my function is a 64-bit integer. My test cannot possibly try every possible 64-bit integer. It would take years for such a test to finish.

This is why tools like formal verification and symbolic analyses can help you establish that for all possible integers X, your function does the right thing (for some definition of “right”). You get this assurance without having to actually enumerate all X.

Re: Verus: Verified Rust for low-level systems code

#46

Post by stephencanon »

sangel wrote: post #45
worldsavior wrote: post #44

Earlier quoted context omitted.

Can't you make the tests check every input? (This is also what they're supposed to do.)

Obviously not. Suppose the input to my function is a 64-bit integer. My test cannot possibly try every possible 64-bit integer. It would take years for such a test to finish. This is why tools like formal verification and symbolic analyses can help you establish that for all possible integers X, your function does the right thing (for some definition of “right”). You get this assurance without having to actually enum…

Indeed. Exhaustively testing a 64b input space requires about 600 machine years for each nanosecond that the function under test takes to run. So, _very_ short-running critical functions are testable on a cluster, but not efficiently testable, and if a function is simple enough to be testable, then it's usually easier to prove that it's correct instead.

Re: Verus: Verified Rust for low-level systems code

#47

Post by vacuity »

pcwalton wrote: post #40
daxfohl wrote: post #18

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?

My feeling is that dependent types add complexity to a language that's already well-known for having a complex type system, so I'm nervous about blowing the complexity budget. But I'm bullish on tools like Verus, Prusti, and Creusot because they allow people who need to write low-level unsafe code to prove their code safe, while keeping the complexity of the safety proofs localized to that code, so most Rust programm…

Agreed. Rust is on track to becoming a practical language for many verification projects. If necessary, perhaps a dialect that focuses on verification could be made and separately maintained (it would probably cut out a lot of normal Rust), or one would just switch to a different technology.

Re: Verus: Verified Rust for low-level systems code

#48

Post by imtringued »

giltho wrote: post #11
weinzierl wrote: post #3

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.

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.

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.

Re: Verus: Verified Rust for low-level systems code

#49

Post by imtringued »

worldsavior wrote: post #44
GolDDranks wrote: post #27

Earlier quoted context omitted.

Test verify that the code works on specific inputs. Formal verification checks that it works on every input.

Can't you make the tests check every input? (This is also what they're supposed to do.)

I don't know why you are trolling us. Tests aren't supposed to check every input. The entire point of classic testing is to define static execution traces by hand. That is obviously meant to only cover a finite number of execution traces. Even 100% test coverage doesn't give you proof over all possible execution traces. Tests prove that the software "works", but they do not prove the absence of bugs (which inherently requires you to specify what a "bug" is, hence the need for a specification).

Not only is static verification more powerful, there is also a massive usability difference. You define your pre and post conditions in each function (also known as specification or design contract) and the tool will automatically check that you do not violate these conditions. It solves a very different problem from classic unit or integration tests.

Post reply on HN