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

231–240 of 448 posts

Re: AI will make formal verification go mainstream

#231

Post by Joker_vD »

est wrote: post #227
QuadrupleA wrote: post #203

I don't think formal verification really addresses most day-to-day programming problems: * A user interface is confusing, or the English around it is unclear * An API you rely on changes, is deprecated, etc. * Users use something in unexpected ways * Updates forced by vendors or open source projects cause things to break * The customer isn't clear what they want * Complex behavior between interconnected systems, out…

> An API you rely on changes, is deprecated, etc Formal verification will eventually lead to good, stable API design. > Users use something in unexpected ways > Complex behavior between interconnected systems It happens when there's no formal verification during the design stage. Formal verification literally means cover 100% state changes and for every possible input/output, every execution branch should be tested.

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

Re: AI will make formal verification go mainstream

#236

Post by ehnto »

est wrote: post #227
QuadrupleA wrote: post #203

I don't think formal verification really addresses most day-to-day programming problems: * A user interface is confusing, or the English around it is unclear * An API you rely on changes, is deprecated, etc. * Users use something in unexpected ways * Updates forced by vendors or open source projects cause things to break * The customer isn't clear what they want * Complex behavior between interconnected systems, out…

> An API you rely on changes, is deprecated, etc Formal verification will eventually lead to good, stable API design. > Users use something in unexpected ways > Complex behavior between interconnected systems It happens when there's no formal verification during the design stage. Formal verification literally means cover 100% state changes and for every possible input/output, every execution branch should be tested.

100% of state changes in business software is unknowable on a long horizon, and relies on thoroughly understanding business logic that is often fuzzy, not discrete and certain.

Re: AI will make formal verification go mainstream

#237

Post by est »

Joker_vD wrote: post #231
est wrote: post #227

Earlier quoted context omitted.

> An API you rely on changes, is deprecated, etc Formal verification will eventually lead to good, stable API design. > Users use something in unexpected ways > Complex behavior between interconnected systems It happens when there's no formal verification during the design stage. Formal verification literally means cover 100% state changes and for every possible input/output, every execution branch should be tested.

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

Re: AI will make formal verification go mainstream

#238

Post by joegibbs »

I think the problem is that people don't know exactly what it is that they want. You could easily make a formally verified application that is nevertheless completely buggy and doesn't make any sense. Like he says about the challenge moving to defining the specification: I don't think that would help because there are fewer people who understand formal verification, who would be able to read that and make sense of it, than there would be people who could write the code.

Re: AI will make formal verification go mainstream

#239

Post by avmich »

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?

It's a bad reason. A lot of best practices are temporary blindnesses, comparable, in some sense, with supposed love to BASIC before or despite Dijkstra. So, yes, it's possible there is no good reason. Though I don't think it's the case here.

Re: AI will make formal verification go mainstream

#240

Post by mrkeen »

pron wrote: post #90
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…

> to me it seems like high-level programming languages are already close to a specification language They are not. The power of rich and succinct specification languages (like TLA+) comes from the ability to succinctly express things that cannot be efficiently computed, or at all. That is because a description of what a program does is necessarily at a higher level of abstraction than the program (i.e. there are many…

Can TLA+ prove anything about something you specify but don't execute?
Post reply on HN