On: Proving a Computer Program's Correctness

[stcredzero]

I was using 'assumption' to talk about the faith that abstractions and their (sometimes mathematical) assumptions can be successfully applied to solve real-world problems.

Some may argue that there's no guarantee that such proofs apply to real world systems. But really, there's no guarantee that any abstract model does. We humans have to get paid for something.

[gdp → stcredzero]

> Some may argue that there's no guarantee that such proofs apply to real world systems.

I would argue that those who would argue that have probably not spent a lot of time doing any real-world formal verification.

People seem to like arguing about its utility in the abstract without ever doing it.

[stcredzero → gdp]

You might be replying as if I'm disagreeing. If so, please re-read ancestor posts with the other spin.

In short: most of the objections people have to formal verification also apply to modeling something in software to begin with.

[gdp → stcredzero]

No, I wasn't suggesting you were disagreeing, I was simply responding to your hypothetical disagreement that some might argue. My counter-argument could be just as applicable to any of the people who have professed similar beliefs to the ones you speculated that some may hold.

[stcredzero → gdp]

It's not so hypothetical. It's more the typical response of a programmer when formal methods come up. But I meant it as an observation of typical reactions, not as a hypothetical debate.