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

AI will make formal verification go mainstream

martin.kleppmann.com

Post reply on HN
Print view View original

311–320 of 448 posts

Re: AI will make formal verification go mainstream

#311

Post by wombatpm »

est wrote: post #237
Joker_vD wrote: post #231

Earlier quoted context omitted.

> Formal verification will eventually lead to good, stable API design. Why? Has it ever happened like this? Because to me it would seem that if the system verified to work, then it works no matter how API is shaped, so there is no incentive to change it to something better.

> if the system verified to work, then it works no matter how API is shaped That's the case for one-off integrations, but the messy part always comes when system goal changes Let's say formal verification could help to avoid some anti-patterns.

Isn’t this where the Eiffel design by contract people speak up about code reuse?

Re: AI will make formal verification go mainstream

#312

Post by mkagenius »

jazzyjackson wrote: post #114
mccoyb wrote: post #83

Earlier quoted context omitted.

If you're maxing out the plans across the platforms, that's 600 bucks -- but if you think about your usage and optimize, I'm guessing somewhere between 200-600 dollars per month.

It's pretty easy to hit a couple hundred dollars a day filling up Opus's context window with files. This is via Anthropic API and Zed. Going full speed ahead building a Rails app from scratch it seemed like I was spending $50/hour, but it was worth it because the App was finished in a weekend instead of weeks. I can't bear to go in circles with Sonnet when Opus can just one shot it.

Anthropic via Azure has sent me an invoice of around $8000 for 3-5 days of Opus 4.1 usage and there is no way to track how many tokens during those days and how many cached etc. (And I thought its part of the azure sponsorship but that's another story)

Re: AI will make formal verification go mainstream

#313

Post by gf000 »

blub wrote: post #270
gizmo686 wrote: post #211

Earlier 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. 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…

> but one reaps the benefits later thanks to more confidence when refactoring or adding code.

To be honest, I believe it makes refactoring/maintenance take longer. Sure, safer, but this is not a one-time only price.

E.g. you decide to optimize this part of the code and only return a reference or change the lifetime - this is an API-breaking change and you have to potentially recursively fix it. Meanwhile GC languages can mostly get away with a local-only change.

Don't get me wrong, in many cases this is more than worthwhile, but I would probably not choose rust for the n+1th backend crud app for this and similar reasons.

Re: AI will make formal verification go mainstream

#314

Post by sothatsit »

blub wrote: post #302
lukan wrote: post #282

Earlier quoted context omitted.

"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 i…

Or: I’m not going to do this refactor at all, even though it would improve the codebase, because it will be near impossible to ensure everything is correct after making so many changes.

To me, this has been one of the biggest advantages of both tests and types. They provide confidence to make changes without needing to be scared of unintended breakages.

Re: AI will make formal verification go mainstream

#315

Post by gf000 »

blub wrote: post #306
teiferer wrote: post #277

Earlier quoted context omitted.

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

Constraints Liberate, Liberties Constrain. (I also recommend watching the presentation with the same title)

Re: AI will make formal verification go mainstream

#316

Post by gf000 »

mplewis wrote: post #220
devin wrote: post #216

Earlier quoted context omitted.

> No one claims that good type systems prevent buggy software. But, they do seem to improve programmer productivity. They really don’t. How did you arrive at such a conclusion?

Through empirical evidence? Do you think that the vast majority of software devs moved to typing for no reason?

We don't actually have empirical evidence on the topic, surprisingly.

It's just people's hunches.

Re: AI will make formal verification go mainstream

#317

Post by jessoteric »

Joker_vD wrote: post #309
est wrote: post #286

Earlier quoted context omitted.

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

> Of course, you can declare that the world itself is inherently sinful and imperfect, and is not ready for your beautiful theories

i see we are both familiar with haskellers (friendly joke!)

Re: AI will make formal verification go mainstream

#319

Post by ad_hockey »

socketcluster wrote: post #81
bkettle wrote: post #61

I think formal verification shines in areas where implementation is much more complex than the spec, like when you’re writing incomprehensible bit-level optimizations in a cryptography implementation or compiler optimization phases. I’m not sure that most of us, day-to-day, write code (or have AI write code) that would benefit from formal verification, since to me it seems like high-level programming languages are al…

Yes. I feel like people who are trying to push software verification have never worked on typical real-world software projects where the spec is like 100 pages long and still doesn't fully cover all the requirements and you still have to read between the lines and then requirements keep changing mid-way through the project... Implementing software to meet the spec takes a very long time and then you have to invest a…

I agree that trying to produce this sort of spec for the entire project is probably a fool's errand, but I still see the value for critical components of the system. Formally verifying the correctness of balance calculation from a ledger, or that database writes are always persisted to the write ahead log, for example.

Re: AI will make formal verification go mainstream

#320

Post by jonathanstrange »

egwor wrote: post #289
rixed wrote: post #281

Earlier quoted context omitted.

And one can see how quickly they became mainstream...

I think that’s because the barrier to entry for a beginner is much higher than say python.

IMHO, these strong type systems are just not worth it for most tasks.

As an example, I currently mostly write GUI applications for mobile and desktop as a solo dev. 90% of my time is spent on figuring out API calls and arranging layouts. Most of the data I deal with are strings with their own validation and formatting rules that are complicated and at the same time usually need to be permissive. Even at the backend all the data is in the end converted to strings and integers when it is put into a database. Over-the-wire serialization also discards with most typing (although I prefer protocol buffers to alleviate this problem a bit).

Strong typing can be used in between those steps but the added complexity from data conversions introduces additional sources of error, so in the end the advantages are mostly nullified.

Post reply on HN