Hacker News Reader

Comment by GregarianChild | Hacker News Reader

> "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.

View on HN

> 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