Hacker News Reader

Comment by erik_seaberg | Hacker News Reader

I learned some TLA+ and started reading about Coq, but I was pretty disappointed to learn of the "verification gap" between the the algorithm to be delivered in a normal programming language and the manually-restated algorithm that passed the checker. We need to make a checker's input language ergonomic enough for daily use and then "synthesize" something that runs efficiently while still being known correct, or make a checker understand everyday programs (which, not being so minimalist, probably have a much larger space of reachable states to check).

View on HN

Yep, I have the same impression. Anything that proves something about stuff that's not the actual running code is nearly useless to me. The code will be changed every single day by developers who may not be familiar with that code. The verification must work on that implementation code.

As I see it, the only way to do it properly is to embed the proof in the code like we embed types in the code. For example, we've been able to get rid of NullPointerException completely by using the checker framework, all we need to do is maunually annotate all values that may be null (everything else is assumed non-null, if you try to assign it to null the compiler won't compile):

    @Nullable String getSomething();

The annotation is not a layer on top of the code, it is code. The compiler can check it (with appropriate extensions).

I even played with adding support for dependent types, I am convinced the compiler extension would allow me to do that, but unfortunately I have other things to do.

This is my biggest gripe with verification. I am hoping that LLMs help with inferring intent from a subroutine, then asking the programmer if the inferred intent is complete and correct, and then automatically writing/updating a verification harness.

What makes you think autocomplete on steroids with no internal reasoning capability or representation of knowledge would be at all useful for inferring intent? Or have you been fooled into thinking an LLM is something like Eurisko/Cyc?

Because ideally good code should make the intent obvious from the names and comments, so inferring a full description should really just be an autocomplete task.

The topic is using an LLM to learn a codebase one doesn’t understand. Does that sound like a codebase that has names and comments from which a full description could be inferred?

Personally I'm with the parent poster - I use LLMs to help me with intent in new codebases I don't understand yet all the time, and empirically they seem to understand it pretty well. Useful, especially when you don't have good documentation on hand.

Boy it sure is useful that you can trust code you don’t understand to have clear variable names and comments for the LLM to key off of.

Clear variable names and comments aren't a requirement at all.

It sounds to me like you have a philosophical problem with LLMs, which is something I don't think we can debate in good faith. I can just share my experience, which is that they are excellent tools for this kind of thing. Obvious caveats apply - only a fool would rely entirely on an LLM without giving it any thought of their own.

I don’t have a philosophical problem with LLMs. I have a problem with treating LLMs as something other than what they are: Predictive text generators. There’s no understanding beneath that which informs the generation, just compression techniques that arise as part of training. Thus I wouldn’t trust them for anything except churning out plausibly-structured text.

Have a look at Eureka, they use a combo of LLMs and basic evolutionary methods to automate solving reinforcement learning problems. What's interesting is that the only human input is the code for the environment of the RL problem and some fixed scaffolding prompts for the GA.

Sounds like it could be a good starting point for something like this.

It would be lovely if Kani and/or Prusti could cope with more realistic code, but they are where my current hopes lie in eliminating the verification gap. The proof is built from (very!) simple functions written in a subset of Rust. If that manages to get to you all the way to the end result, then there was no gap.

https://github.com/model-checking/kani

http://prusti.org/

Reply on news.ycombinator.com