Hacker News Reader

Comment by xavxav | Hacker News Reader

> You can knock off most things you have to prove with a SAT solver. But you'll need something heavier for the hard problems. Coq is too manual. The author thinks ACL2 is too functional. Not sure what to do there, but I've been out of this for decades.

Agreed, though I think Lean is making big progress in the UX front of ITP verification through its extensive meta-programming facilities.

My issue with these tools applied to verifying external languages like Rust, is that the proof is not written in the target language, forcing your developers to learn two languages.

I have recently been thinking about what a "verification aware Rust" would look like, colored by my experience writing Creusot, the work on Verus and Aeneas and my time in the lab developing Why3. I think building such a language from the ground up could provide a step change in ease of verification even from Rust, particularly with regard to those "hard parts" of the proof.

View on HN

> "verification aware Rust" ... building such a language from the ground up could

Could you sketch in a few bullet point what you think is missing and how to fix the gaps?

In my experience a core problem is that adding rich specifications slows down rapid evolution of programs, since the proliferate transitively along the control flow graphs. We can see this most prominently with Java's checked exceptions, but most effect annotations (to give an example of simple specification annotations) suffer from the same cancerous growth. This is probably at least partly intrinsic, but it could be improved by better automation.

> Could you sketch in a few bullet point what you think is missing and how to fix the gaps?

Not yet, I am planning on writing some blog posts about it but there are still enough fuzzy points I don't want to share yet.

> ... since the proliferate transitively along the control flow graphs. ... suffer from the same cancerous growth.

This is one of the biggest and most difficult issues of verification, I fully agree. The 'promise' of verified code is that you don't need to understand the code, you can just look at the smaller, higher-level spec, but right now verified code has a specification & proof overhead > 1, it needs to drop to < 0.1 for it to become economical.

To me at least, the most difficult part of verifying rust code has been the lack of any pre/post conditions on the standard library, I quite often have ended up rewriting chunks of the std library, pulling them directly into my program to verify them.

I personally think it would be interesting if we had a nightly-only/unstable pre/post conditions in the std library. Then one could take the commit of the compiler that corresponds to a stable release and verify against that. That is the overhead I seem to be bumping my head against whenever I try to verify some rust code at least.

Since learning Eiffel in the 90's I keep looking forward for them to become mainstream, beyond the typical assert like statements.

So far we had annotations in Java (which required additional tooling and never took off), .NET (hidden behind enterprise license, thus hardly adopted), D (which suffers from adoption), Common Lisp (nice, but again adoption issues), Ada (again the language adoption), C++26 (if they actually land, and only as MVP)

Almost 40 years later, and still no good story for DbC.

Yes, keep plugging on that one. Verification statements should be in the same language as the program, and be syntax and type checked on every compile. Not in comments. That keeps them consistent with the code.

Sorry that this is a very basic question but I never had any of this in uni and I find it super exciting:

If I am trying to prove something I can state in my target language how would statement and proof differ?

If the thing to prove is not expressible in the target language (e.g. the fact that a function terminates) I would have to use a separate language anyway.

Could you give an example how this could hypothetically look like (preferably in pseudo Rust)?

Different user, but sure! Three examples:

1) you might have two algorithms for computing the same thing, one simple and obviously right, and one complex and optimized. So you want to state that they always produce the same thing.

  fn my_complex_algo(x : Input) -> o:Output ensures o == simple_algo(x)

2. You might have high level "properties" you want to be true about your program. For example, a classic property about type-checkers is that they are "sound" (meaning that if you say a program is well typed, then when you run it it must be impossible to get a type error).

3. You might have really simple properties you want to prove, for example that an "unreachable!()" is indeed actually unreachable.

> you might have two algorithms for computing the same thing, one simple and obviously right, and one complex and optimized.

Right. Those are the kinds of systems that are easy to specify concisely. Databases, for example, can be specified as giant arrays with linear search.

Reply on news.ycombinator.com