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

Long division verified via Hoare logic

cofault.com

Post reply on HN
Print view View original

11–20 of 63 posts

Re: Long division verified via Hoare logic

#11

Post by unification_fan »

AnimalMuppet wrote: post #6
unification_fan wrote: post #3

Earlier quoted context omitted.

Why should it save labor. What it does is guarantee correctness which is like the holy grail for programmers. If you know shit's correct you can just assume stuff and it will actually work on the first try. You don't even need to write tests for it.

Because it takes so much work . Good software, even with bugs, released today, can be used today. Perfect software, released two years from now, cannot be used today, or next week, or next year. "Good now" beats "perfect later", at least now, but often it beats it later too. While someone is working on "provably perfect", someone who isn't using that approach has released four versions that were not perfect, but were…

But you don't have to do the proving. You can let someone who is, like, REALLY good at formal verification do it and then benefit from the libraries they produce

Verification is useful when you're dealing with low level or very declarative stuff. You don't really have to "verify" a CRUD repository implementation for a random SPA. But the primitives it relies on, it would be good if those were verified.

Re: Long division verified via Hoare logic

#12

Post by unification_fan »

kimixa wrote: post #7
AnimalMuppet wrote: post #6

Earlier quoted context omitted.

Because it takes so much work . Good software, even with bugs, released today, can be used today. Perfect software, released two years from now, cannot be used today, or next week, or next year. "Good now" beats "perfect later", at least now, but often it beats it later too. While someone is working on "provably perfect", someone who isn't using that approach has released four versions that were not perfect, but were…

Also "perfect software" doesn't actually mean "perfectly robust systems" - at the end of the day it has to interact with the Real World, and the Real World is messy. You still have to cope with failures from cosmic rays, power brownouts, hardware bugs (or at least a difference in specification of the hardware to the model used for this sort of formal verification), failures communicating with other devices etc. So cr…

> You still have to cope with failures from cosmic rays

Much like you have to cope with hash or GUID collisions... that is, you don't, because it statistically never happens. Unless you're speedrunning super mario or something.

Besides if you have a program that's formally verified, you just need to do what NASA did for its Apollo missions and make all the logic redundant and gate it behind a consensus algorithm.

You can argue that all 4 computers might get hit by a cosmic ray in just the right place and at just the right time... But it will never ever happen in the history of ever.

So my point is that the real world is messy. But the systems we design as engineers are not necessarily as messy. And the interface between the real world and our systems can be managed, and the proof of it is that we wouldn't be chatting across an entire ocean by modulating light itself if that weren't the case.

Re: Long division verified via Hoare logic

#13

Post by AnimalMuppet »

unification_fan wrote: post #11
AnimalMuppet wrote: post #6

Earlier quoted context omitted.

Because it takes so much work . Good software, even with bugs, released today, can be used today. Perfect software, released two years from now, cannot be used today, or next week, or next year. "Good now" beats "perfect later", at least now, but often it beats it later too. While someone is working on "provably perfect", someone who isn't using that approach has released four versions that were not perfect, but were…

But you don't have to do the proving. You can let someone who is, like, REALLY good at formal verification do it and then benefit from the libraries they produce Verification is useful when you're dealing with low level or very declarative stuff. You don't really have to "verify" a CRUD repository implementation for a random SPA. But the primitives it relies on, it would be good if those were verified.

Same problem. Sure, it would be great if the primitives we use were proven correct. But I've got stuff to write today, and it doesn't look like the proven-correct primitives are going to arrive any time soon. If I wait for them, I'm going to be waiting a long time, with my software not getting written.

Re: Long division verified via Hoare logic

#14

Post by thaumasiotes »

unification_fan wrote: post #3
recursivedoubts wrote: post #2

i think this shows why formal verification, while certainly useful in specialized situations, will likely not be a major boost for software productivity[1] [1] - https://worrydream.com/refs/Brooks_1986_-_No_Silver_Bullet.p... : > I do not believe we will find the magic here. Program verification is a very powerful concept, and it will be very important for such things as secure operating system kernels. The technolog…

Why should it save labor. What it does is guarantee correctness which is like the holy grail for programmers. If you know shit's correct you can just assume stuff and it will actually work on the first try. You don't even need to write tests for it.

> What it does is guarantee correctness which is like the holy grail for programmers.

Formal verification can never guarantee correctness. For that to happen, you'd need to know that the property you verified is the property you want. If you have the ability to write correct specifications, you also have the ability to write correct programs, and running the verification doesn't add any value.

Re: Long division verified via Hoare logic

#15

Post by [deleted] »

recursivedoubts wrote: post #2

i think this shows why formal verification, while certainly useful in specialized situations, will likely not be a major boost for software productivity[1] [1] - https://worrydream.com/refs/Brooks_1986_-_No_Silver_Bullet.p... : > I do not believe we will find the magic here. Program verification is a very powerful concept, and it will be very important for such things as secure operating system kernels. The technolog…

[deleted]

Re: Long division verified via Hoare logic

#16

Post by dwheeler »

recursivedoubts wrote: post #2

i think this shows why formal verification, while certainly useful in specialized situations, will likely not be a major boost for software productivity[1] [1] - https://worrydream.com/refs/Brooks_1986_-_No_Silver_Bullet.p... : > I do not believe we will find the magic here. Program verification is a very powerful concept, and it will be very important for such things as secure operating system kernels. The technolog…

It's widely agreed that formal verification does not boost software productivity, in the sense that formal verification doesn't speed up development of "software that compiles and runs and we don't care if it's correct".

The point of formal verification is to ensure that the software meets certain requirements with near certainty (subject to gamma radiation, tool failure, etc.). If mistakes aren't important, formal verification is a terrible tool. If mistakes matter, then formal verification may be what you need.

What this and other articles show is that doing formal verification by hand is completely impractical. For formal verification to be practical at all, it must be supported by tools that can automate a great deal of it.

The need for automation isn't new in computing. Practically no one writes machine code directly, we write in higher-level languages, or rarely assembly languages, and use automated tools to generate the final code. It's been harder to create practical tools for formal verification, but clearly automation is a minimum requirement.

Re: Long division verified via Hoare logic

#17

Post by nextos »

dwheeler wrote: post #16
recursivedoubts wrote: post #2

i think this shows why formal verification, while certainly useful in specialized situations, will likely not be a major boost for software productivity[1] [1] - https://worrydream.com/refs/Brooks_1986_-_No_Silver_Bullet.p... : > I do not believe we will find the magic here. Program verification is a very powerful concept, and it will be very important for such things as secure operating system kernels. The technolog…

It's widely agreed that formal verification does not boost software productivity, in the sense that formal verification doesn't speed up development of "software that compiles and runs and we don't care if it's correct". The point of formal verification is to ensure that the software meets certain requirements with near certainty (subject to gamma radiation, tool failure, etc.). If mistakes aren't important, formal v…

Automation of Hoare logic is quite good these days. Dafny, from MS Research (https://dafny.org), is probably the most friendly formal language of any kind. It's built around Hoare logic and its extension, separation logic. The barrier of entry is low. A seasoned imperative or functional programmer can get going with Dafny in just a few days. Dafny has been used to verify large systems, including many components of AWS.

I am hoping that LLMs make more advanced languages, such as Liquid Haskell or Agda, less tedious to use. Ideally, lots of code should be autocompleted once a human provides a type signature. The advantage of formal verification is that we can be sure the generated code is correct.

Re: Long division verified via Hoare logic

#18

Post by rocqua »

thaumasiotes wrote: post #14
unification_fan wrote: post #3

Earlier quoted context omitted.

Why should it save labor. What it does is guarantee correctness which is like the holy grail for programmers. If you know shit's correct you can just assume stuff and it will actually work on the first try. You don't even need to write tests for it.

> What it does is guarantee correctness which is like the holy grail for programmers. Formal verification can never guarantee correctness. For that to happen, you'd need to know that the property you verified is the property you want. If you have the ability to write correct specifications, you also have the ability to write correct programs, and running the verification doesn't add any value.

Correctness is taken to mean "The program matches its specification". Or, more literally, "the program is a correct implementation of it's specification".

Re: Long division verified via Hoare logic

#19

Post by AlotOfReading »

unification_fan wrote: post #12
kimixa wrote: post #7

Earlier quoted context omitted.

Also "perfect software" doesn't actually mean "perfectly robust systems" - at the end of the day it has to interact with the Real World, and the Real World is messy. You still have to cope with failures from cosmic rays, power brownouts, hardware bugs (or at least a difference in specification of the hardware to the model used for this sort of formal verification), failures communicating with other devices etc. So cr…

> You still have to cope with failures from cosmic rays Much like you have to cope with hash or GUID collisions... that is, you don't, because it statistically never happens. Unless you're speedrunning super mario or something. Besides if you have a program that's formally verified, you just need to do what NASA did for its Apollo missions and make all the logic redundant and gate it behind a consensus algorithm. You…

I've definitely dealt with hash/GUID collisions in the context of safety critical systems before. It's not a particularly uncommon requirement either.

"just" is pulling a lot of weight in your comment. Redundant consensus is difficult and expensive, all to address very particular error models (like the one you're assuming). If we expand our error model from localized error sources like cosmic rays to say, EMI, there are entire categories of fault injection attacks well-known to work against modern redundant systems.

That's assuming your specification is comprehensive and correct in the first place of course. My experience is that all specifications have holes related to their assumptions about the real world, and many of them have bugs or unintended behavior as well.

Re: Long division verified via Hoare logic

#20

Post by LegionMammal978 »

rocqua wrote: post #18
thaumasiotes wrote: post #14

Earlier quoted context omitted.

> What it does is guarantee correctness which is like the holy grail for programmers. Formal verification can never guarantee correctness. For that to happen, you'd need to know that the property you verified is the property you want. If you have the ability to write correct specifications, you also have the ability to write correct programs, and running the verification doesn't add any value.

Correctness is taken to mean "The program matches its specification". Or, more literally, "the program is a correct implementation of it's specification".

Taking the reductio ad absurdum, the program itself perfectly specifies its own behavior. Yet it's hardly something I'd point to as a holy grail. We want programs that do what we want them to, which is generally a human construct rather than a technical one. (And you'd better hope that two different people don't expect the program to do two different things in the same situation!)
Post reply on HN