I will respectfully take the other side of this bet on polymarket if it ever shows up.
AI will make formal verification go mainstream
301–310 of 448 posts
Re: AI will make formal verification go mainstream
#302Earlier quoted context omitted.
> No one claims that good type systems prevent buggy software. But, they do seem to improve programmer productivity. To me it seems they reduce productivity. In fact, for Rust, which seems to match the examples you gave about locks or regions of memory the common wisdom is that it takes longer to start a project, but one reaps the benefits later thanks to more confidence when refactoring or adding code. However, even…
"In my experience, the more information is encoded in the type system, the more effort is required to change code." Have you seen large js codebases? Good luck changing anything in it, unless they are really, really well written, which is very rare. (My own js code is often a mess) When you can change types on the fly somewhere hidden in code ... then this leads to the opposite of clarity for me. And so lots of effor…
There’s two types of slowdown at play:
a) It’s fast to change the code, but now I have failures in some apparently unrelated part of the code base. (Javascript) and fixing that slows me down.
b) It’s slow to change the code because I have to re-encode all the relationships and semantic content in the type system (Rust), but once that’s done it will likely function as expected.
Depending on project, one or the other is preferable.
Re: AI will make formal verification go mainstream
#303Earlier quoted context omitted.
> Let's say formal verification could help to avoid some anti-patterns. I'd still like to hear about the actual mechanism of this happening. Because I personally find it much easier to believe that the moment keeping the formal verification up to date becomes untenable for whatever reason (specs changing too fast, external APIs to use are too baroque, etc) people would rather say "okay, guess we ditch the formal veri…
> I'd still like to hear about the actual mechanism of this happening I am not an expert on this, but the worst API I've seen is those with hidden states. e.g. .toggle() API. Call it old number of times, it goes to one state, call it even number of times, it goes back. And there's call A before you call B types of APIs, the client has to keep a strict call order (which itself is a state machine of some kind)
> I am not an expert on this, but the worst API I've seen is those with hidden states.
> e.g. .toggle() API. Call it old number of times, it goes to one state, call it even number of times, it goes back.
This is literally a dumb light switch. If you have trouble proving that, starting from lights off, flicking a simple switch twice will still keep lights off then, well, I have bad news to tell you about the feasibility of using the formal methods for anything more complex than a dumb light switch. Because the rest of the world is a very complex and stateful place.
> (which itself is a state machine of some kind)
Yes? That's pretty much the raison d'être of the formal methods: for anything pure and immutable, normal intuition is usually more than enough; it's tracking the paths through enormous configuration spaces that our intuition has problem with. If the formal methods can't help with that with comparable amount of effort, then they are just not worth it.
Re: AI will make formal verification go mainstream
#304I've been heearing about formal verification since college (which for me was more than 30 years ago) and I even taught a thing called "Z", which was a formally verifiable academia thing that tried to be the ultimate formal language. It never panned out, and I honestly don't think that AI is going to help in anything but test generation, which is going to remain the most pragmatic approach to formal verification (but, like all things, it's an approximation, not 100% correct).
Re: AI will make formal verification go mainstream
#305> As the verification process itself becomes automated, the challenge will move to correctly defining the specification: that is, how do you know that the properties that were proved are actually the properties that you cared about? Reading and writing such formal specifications still requires expertise and careful thought. But writing the spec is vastly easier and quicker than writing the proof by hand, so this is p…
And yet code is being written and deployed to prod all the time, with many layers of tests. Formal specs can be used at least at all the same levels, but crucially also at the technical docs level. LLMs make writing them cheap. What’s not to like?
Re: AI will make formal verification go mainstream
#306Earlier quoted context omitted.
> No one claims that good type systems prevent buggy software. But, they do seem to improve programmer productivity. To me it seems they reduce productivity. In fact, for Rust, which seems to match the examples you gave about locks or regions of memory the common wisdom is that it takes longer to start a project, but one reaps the benefits later thanks to more confidence when refactoring or adding code. However, even…
> In my experience, the more information is encoded in the type system, the more effort is required to change code. I would tend to disagree. All that information encoded in the type system makes explicit what is needed in any case and is otherwise only carried informally in peoples' heads by convention. Maybe in some poorly updated doc or code comment where nobody finds it. Making it explicit and compiler-enforced i…
In practice it would be encoded in comments, automated tests and docs, with varying levels of success.
It’s actually similar to tests in a way: they provide additional confidence in the code, but at the same time ossify it and make some changes potentially more difficult. Interestingly, they also make some changes easier, as long as not too many types/tests have to be adapted.
Re: AI will make formal verification go mainstream
#307Earlier quoted context omitted.
A limited form of formal verification is already mainstream. It is called type systems. The industry in general has been slowly moving to encode more invariants into the type system, because every invariant that is in the type system is something you can stop thinking about until the type checker yells at you. A lot of libraries document invariants that are either not checked at all, only at runtime, or somewhere in…
> No one claims that good type systems prevent buggy software. That's exactly what languages with advanced type systems claim. To be more precise, they claim to eliminate entire classes of bugs. So they reduce bugs, they don't eliminate them completely.
No nulls, no nullability bombs.
Forcing devs to pre-fix/avoid bugs before the compiler will allow the app means the programs are more correct as a group.
Wrong, incomplete, insufficient, unhelpful, unimpressive, and dumb are all still very possible. But more correct than likely in looser systems.
Re: AI will make formal verification go mainstream
#308It absolutely will not make formal verification go mainstream.
What it will make go mainstream, and in fact has already started to, is “ChatGPT verified it so it must be OK.”
Re: AI will make formal verification go mainstream
#309Earlier quoted context omitted.
Formal verification has nothing to do with the quality of the API. Given the spec, formal verification can tell you if your implementation follows the spec. It cannot tell you if the spec if good
> It cannot tell you if the spec if good I beg to differ, if a spec is hard to verify, then it's a bad sign.
All non-trivial specs, like the one for seL4, are hard to verify. Lots of that complexity comes from interacting with the rest of the world which is a huge shared mutable global state you can't afford to ignore.
Of course, you can declare that the world itself is inherently sinful and imperfect, and is not ready for your beautiful theories but seriously.
Re: AI will make formal verification go mainstream
#310Earlier quoted context omitted.
Google denies qualified people all the time. They would much rather reject a great hire than take a risk on accepting a mediocre one. I feel for him but it's just the nature of the beast. Not everyone will get in.
I've heard this before. Why do you think algorithm questions are effective for finding "good" hires? Are they ?
They certainly don't filter out toxic people who make others leave companies because they poison the well.