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

What can you confidently guarantee about your software?

queue.acm.org

Post reply on HN
Print view View original

21–30 of 71 posts

Re: What can you confidently guarantee about your software?

#21

Post by nilkn »

dfabulich wrote: post #2

Formal verification is still too limited to be useful for most app developers. The article gives an example of an e-commerce platform using it to prove the correctness of managing refunds, but then acknowledges: > As of today, the formally verified core can handle most effect-free logic—invariants, transitions, conflict resolution. But the UI, network calls, and database interactions typically sit outside the verific…

There's a lot of really important software out there where being able to easily verify effect-free core logic would certainly be very useful. An e-commerce web app is not a good example. Anything safety-critical -- aerospace, defense, medical devices, power generation, industrial machines -- already requires a certification process. Auto-generating proof evidence as part of the cert process (which generally requires a rigorous spec anyway) in the near future seems like a no brainer.

Re: What can you confidently guarantee about your software?

#22

Post by AnimalMuppet »

taeric wrote: post #18

I'm not entirely sure what this is showing people don't understand? Especially when going with such silly ill defined concepts as "financial conservation". Just what? Now model in that it was shipped, but an earthquake caused the delivery truck to be destroyed. Or it was shipped, but the person that ordered passed away before delivery and the estate is refusing to accept packages. People will want to somehow transfer…

What I think I hear you saying is, do formal verification as much as you can. But also remember that that's never 100%, and therefore you need to leave some kind of escape hatch or alternate process or something.

Re: What can you confidently guarantee about your software?

#23

Post by win311fwg »

dfabulich wrote: post #2

Formal verification is still too limited to be useful for most app developers. The article gives an example of an e-commerce platform using it to prove the correctness of managing refunds, but then acknowledges: > As of today, the formally verified core can handle most effect-free logic—invariants, transitions, conflict resolution. But the UI, network calls, and database interactions typically sit outside the verific…

> Formal verification is still too limited to be useful for most app developers

Limited formal verification is useful to most app developers. Consider a simplistic system that requires you to specify variables as strings or integers. You've almost certainly used a language that can express that before. Being able to formally verify that you haven't tried to stuff a string into an integer in order to give your editor the squiggles is a productivity enhancer. Or used to be in the pre-vibe coding days, at least; who knows anymore.

Your tests will eventually tell you the same thing, that is true, but the industry has decided that there is little downside to having at least some degree of formal verification and a whole lot of upsides. The question is always: where do the returns diminish? This is where you get the silly commentary on HN with the Rust guys crying out that Go isn't expressive enough and the Rocq guys laughing at it all.

Re: What can you confidently guarantee about your software?

#24

Post by AnimalMuppet »

toast0 wrote: post #9
dfabulich wrote: post #2

Formal verification is still too limited to be useful for most app developers. The article gives an example of an e-commerce platform using it to prove the correctness of managing refunds, but then acknowledges: > As of today, the formally verified core can handle most effect-free logic—invariants, transitions, conflict resolution. But the UI, network calls, and database interactions typically sit outside the verific…

The first part of formal verification is getting a formal specification. I don't know about most developers, but I rarely get a written specification for anything I work on, and when I do, it's no where near what would be needed to turn it into a formal specification. Anyway, the specification is subject to change at the whim of a hat, so putting a lot of effort into verifying it is foolish. I do see value in formal…

At my last job, I got a formal specification for one project. But the implementation happened in parallel for time reasons, so by the time the spec was frozen, 90% of the code was written.

Re: What can you confidently guarantee about your software?

#25

Post by derdi »

toast0 wrote: post #9
dfabulich wrote: post #2

Formal verification is still too limited to be useful for most app developers. The article gives an example of an e-commerce platform using it to prove the correctness of managing refunds, but then acknowledges: > As of today, the formally verified core can handle most effect-free logic—invariants, transitions, conflict resolution. But the UI, network calls, and database interactions typically sit outside the verific…

The first part of formal verification is getting a formal specification. I don't know about most developers, but I rarely get a written specification for anything I work on, and when I do, it's no where near what would be needed to turn it into a formal specification. Anyway, the specification is subject to change at the whim of a hat, so putting a lot of effort into verifying it is foolish. I do see value in formal…

Nitpick: You don't necessarily need any specification at all in order to reap benefits. Formal verification languages come with a lot of conditions that your program must fulfill in order to be accepted: Every loop terminates, every object you want to read/write is non-null, every list or array access is in bounds, etc.

For example, if you load an arbitrary C program into Frama-C, you'll have tons of properties to prove before you can even think of adding your own specification. The promises you get is that the program will always terminate and will never invoke undefined behavior. These properties are extremely useful, and these requirements are unlikely to change! And yes, C is... special. But pretty much any language has lists or arrays, nullable/option types, and unbounded loops. "No crashes/panics/uncaught exceptions" should be worth it.

And then, even absent a specification, you can start modeling invariants of the system anyway. This list is always sorted, this number is always strictly positive, this data structure never contains duplicate entries, etc. Anything that today would be a comment saying: "Important! The caller must ensure that..." This can help you gain confidence in your system. And if some day a requirement comes along that really requires you to violate one of these invariants, well, you can just remove it, the same way you would remove a test that no longer reflects something that should hold.

Re: What can you confidently guarantee about your software?

#26

Post by taeric »

AnimalMuppet wrote: post #22
taeric wrote: post #18

I'm not entirely sure what this is showing people don't understand? Especially when going with such silly ill defined concepts as "financial conservation". Just what? Now model in that it was shipped, but an earthquake caused the delivery truck to be destroyed. Or it was shipped, but the person that ordered passed away before delivery and the estate is refusing to accept packages. People will want to somehow transfer…

What I think I hear you saying is, do formal verification as much as you can. But also remember that that's never 100%, and therefore you need to leave some kind of escape hatch or alternate process or something.

Absolutely! I always have worries when posting on my personal doubts on any technique, as I genuinely look forward to people making progress in spite of my doubts.

Re: What can you confidently guarantee about your software?

#27

Post by win311fwg »

dfabulich wrote: post #17
gf000 wrote: post #8

Earlier quoted context omitted.

Well, I'm someone who barely knows more than jack about formal verification, but in pretty much every case you have to have some kind of model that you are actually verifying. How close that model sits to the real thing you have modeled is an important question, and you are free to be as close or distant as you want -- e.g. for verifying different properties of a programming language you might decide to not care abou…

Formal verification is a siren song. The siren sings, "bug-free code is possible in principle!" But it's a trap. Even with LLMs, bug-free code is impractical. I argued that property-based testing is mostly unhelpful for e-commerce/CRUD apps, and that formal verification is a performance improvement on property-based tests. In a property-based test, you identify some rule (an invariant) that you want to apply to your…

> An actual rule that should always be followed, inflexibly, such that a mathematical proof would be useful (and that actually matters to your business) is so rare in CRUD apps that I'm not sure I've ever seen one.

I see them often. Nearly every CRUD app I have come across in the wild has, for example, employed some form of email validation. To your concern, the rules of email validation are well defined and are unlikely to ever change. Importantly, a large percentage of the implementations I saw got it wrong.

As a user, I have also tried to use CRUD apps that have rejected my valid email address, so this isn't even a class of problems that will never be realized in practice. It is a pain I have felt in the real world. The use of PBTs or proofs would have easily uncovered the implementation failures.

Re: What can you confidently guarantee about your software?

#28

Post by dfabulich »

win311fwg wrote: post #27
dfabulich wrote: post #17

Earlier quoted context omitted.

Formal verification is a siren song. The siren sings, "bug-free code is possible in principle!" But it's a trap. Even with LLMs, bug-free code is impractical. I argued that property-based testing is mostly unhelpful for e-commerce/CRUD apps, and that formal verification is a performance improvement on property-based tests. In a property-based test, you identify some rule (an invariant) that you want to apply to your…

> An actual rule that should always be followed, inflexibly, such that a mathematical proof would be useful (and that actually matters to your business) is so rare in CRUD apps that I'm not sure I've ever seen one. I see them often. Nearly every CRUD app I have come across in the wild has, for example, employed some form of email validation. To your concern, the rules of email validation are well defined and are unli…

The rules of email validation are not remotely well defined! Syntactic email validation is an impossibly hard problem. https://www.netmeister.org/blog/email.html

IMO the industry consensus is never to "validate" email addresses syntactically, but simply to ensure that the email address contains at least one @ and to verify the email address by emailing it an activation code.

Proofs would not have uncovered these failures. The proofs would have proved that they rejected your email address as invalid, and the developers would have patted themselves on the back for a job well done.

Re: What can you confidently guarantee about your software?

#29

Post by win311fwg »

dfabulich wrote: post #28
win311fwg wrote: post #27

Earlier quoted context omitted.

> An actual rule that should always be followed, inflexibly, such that a mathematical proof would be useful (and that actually matters to your business) is so rare in CRUD apps that I'm not sure I've ever seen one. I see them often. Nearly every CRUD app I have come across in the wild has, for example, employed some form of email validation. To your concern, the rules of email validation are well defined and are unli…

The rules of email validation are not remotely well defined! Syntactic email validation is an impossibly hard problem. https://www.netmeister.org/blog/email.html IMO the industry consensus is never to "validate" email addresses syntactically, but simply to ensure that the email address contains at least one @ and to verify the email address by emailing it an activation code. Proofs would not have uncovered these fail…

> The rules of email validation are not remotely well defined!

RFC 5322 fully defines the structure.

> IMO the industry consensus is never to "validate" email addresses syntactically

That is true, but not because it isn't well defined, but because it is hard to get right. Keep in mind that most developers don't even know what a property-based test is, and of those that do, only a small subset of them know how to use them. If you find any testing around it at all, which is a stretch to begin with, you will be lucky to find more than a small set of common addresses without any care or concern for the complex edge cases that lead to problems like I have had as a user in the past. Encouraging developers to only validate for the presence of @ means that there is no additional room to screw things up.

But better than to rely on gimping your code to deal with developers is to use the tools at your disposal.

> and to verify the email address by emailing it an activation code.

That may also be beneficial, but not for the same reason. Not all CRUD use-cases fit that mould.

Re: What can you confidently guarantee about your software?

#30

Post by dfabulich »

derdi wrote: post #25
toast0 wrote: post #9

Earlier quoted context omitted.

The first part of formal verification is getting a formal specification. I don't know about most developers, but I rarely get a written specification for anything I work on, and when I do, it's no where near what would be needed to turn it into a formal specification. Anyway, the specification is subject to change at the whim of a hat, so putting a lot of effort into verifying it is foolish. I do see value in formal…

Nitpick: You don't necessarily need any specification at all in order to reap benefits. Formal verification languages come with a lot of conditions that your program must fulfill in order to be accepted: Every loop terminates, every object you want to read/write is non-null, every list or array access is in bounds, etc. For example, if you load an arbitrary C program into Frama-C, you'll have tons of properties to pr…

> "No crashes/panics/uncaught exceptions" should be worth it.

Surprisingly, no. Property-based testing and formal validation make it easy to spend tons of time and money "preventing" bugs that would never have occurred in production, especially uncaught exceptions.

There is code where strong guarantees can be worth it, (databases, platforms/operating systems, parsers accepting hostile input) but it's not most application-level code, and certainly not most e-commerce CRUD apps.

Remember, we're here to make users' lives better, not to write correct code for its own sake.

Post reply on HN