> it skips over the one step the industry still refuses to do: decide what the software is supposed to do in the first place.

Not only that, but it's been well-established that a significant challenge with formally verified software is to create the right spec -- i.e. one that actually satisfies the intended requirements. A formally verified program can still have bugs, because the spec (which requires specialized skills to read and understand) may not satisfy the intent of the requirements in some way.

So the fundamental issue/bottleneck that emerges is the requirements <=> spec gap, which closing the spec <=> executable gap does nothing to address. Translating people's needs to an empirical, maintainable spec of one type or another will always require skilled humans in the loop, regardless of how easy everything else gets -- at minimum as a responsibility sink, but even more as a skilled technical communicator. I don't think we realize how valuable it is to PMs/executives and especially customers to be understood by a skilled, trustworthy technical person.

▲

suspended_state 5 days ago | parent | next [-]

> A formally verified program can still have bugs, because the spec (which requires specialized skills to read and understand) may not satisfy the intent of the requirements in some way.

That's not a bug, that's a misunderstanding, or at least an error of translation from natural language to formal language.

Edit:

I agree that one can categorize incorrect program behavior as a bug (apparently there's such a thing as "behavioral bug"), but to me it seems to be a misnomer.

I also agree that it's difficult to tell that to a customer when their expectations aren't met.

▲

gls2ro 5 days ago | parent | next [-]

In some definitions (that I happen to agree with but because we wanted to save money by first not properly training testers and then getting rid of them is not present so much in public discourse) the purpose of testing (or better said quality control) is:

1) Verify requirements => this can be done with formal verifications

2) Validate fit for purpose => this is where we make sure that if the customer needs addition it does not matter if our software does very well substraction and it has a valid proof of doing that according with specs.

I know this second part is kinda lost in the transition from oh my god waterfall is bad to yeyy now we can fire all testers because the quality is the responsibility of the entire team.

▲

AlienRobot 4 days ago | parent | prev [-]

>an error of translation from natural language to formal language

Really? Programming languages are all formal languages, which means all human-made errors in algorithms wouldn't be "bugs" anymore. Some projects even categorize typos as bugs, so that's a unusually strict definition of "bug" in my opinion.

	▲	suspended_state 2 days ago \| parent [-]
		Sure, I guess you can understand what I said that way, but that's not what I meant. I wasn't thinking about the implementation, but the specifications. Read again the quote I was refering to if you need better context to understand my comment. If you have good formal specifications, you should be able to produce the corresponding code. Any error in that phase should be considered a bug, and yes, a typo should fit that category, if it makes the code deviate from the specs. But an error in the step of translating the requirements (usually explained in natural language) to specifications (usually described formally) isn't a bug, it's a translation error.

▲

jandrese 5 days ago | parent | prev [-]

The danger of this is people start asking about formally verified specs, and down that road lies madness.

"If you can formally verify the spec the code can be auto-generated from it."

	▲	TimTheTinker 5 days ago \| parent [-]
		Most formal "specs" (the part that defines the system's actual behavior) are just code. So a formally verified (or compiled) spec is really just a different programming language, or something layered on top of existing code. Like TypeScript types are a non-formal but empirical verification layer on top of JavaScript. The hard part remains: translating from human-communicated requirements to a maintainable spec (formally verified or not) that completely defines the module's behavior.