"Unlike math, software can't be objectively, formally verified to be correct. " brb, changing industry
-
-
Replying to @old_sound
@old_sound@edwinbrady ‘strue. Even if you can verify the software (which is usually impractical) the spec it was written to can’t be.1 reply 0 retweets 0 likes -
Replying to @DrHydeous
@DrHydeous@old_sound It's more complicated than that though. Some bits of spec, like "never access an invalid resource" are pretty clear.1 reply 0 retweets 0 likes -
Replying to @edwinbrady
@edwinbrady@old_sound in real world software that's not clear, because what's invalid for whom when is Complicated.2 replies 0 retweets 0 likes -
Replying to @DrHydeous
@DrHydeous "Array access always in bounds" "Null pointers never dereferenced" "Will halt" - not industry ready yet, but we *can* do this.1 reply 0 retweets 0 likes -
Replying to @edwinbrady
@edwinbrady none of that stuff matters when you have a spec that is unclear or even contradictory. Which is always.2 replies 0 retweets 0 likes -
Replying to @DrHydeous
@DrHydeous If you think verifying those things is pointless, I never want to use your code. And you're just being dismissive, so I'll stop.1 reply 1 retweet 0 likes -
Replying to @edwinbrady
@edwinbrady you're missing my point. Little technical problems like that are insignificant compared to pesky humans writing rubbish specs.1 reply 0 retweets 0 likes -
Replying to @DrHydeous
@DrHydeous I see. But they are different problems. I realise rubbish specs are hard to tackle, but that wasn't the original point.1 reply 0 retweets 0 likes -
Replying to @edwinbrady
@edwinbrady the original point was about objective formal verification of correctness. The measure of correctness is meeting the spec.2 replies 0 retweets 0 likes
@DrHydeous And specs exist on many levels. Some harder to verify than others, some vaguer than others. It's complicated.
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.