"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@edwinbrady Are you saying that a vague spec for business logic makes a segfault OK? Seems like an odd conclusion.1 reply 0 retweets 0 likes -
Replying to @d_christiansen
@d_christiansen@edwinbrady a segfault is like any other bug: acceptability depends on consequences and cost of mitigation. It's not binary.2 replies 0 retweets 0 likes -
Replying to @DrHydeous
@DrHydeous@d_christiansen Well, yes, obviously. You seemed to be dismissing all verification though due to specs being hard.2 replies 0 retweets 0 likes -
Replying to @edwinbrady
@edwinbrady Imagine I offer to fix yr travel from Edinburgh, then just work on the 5 min walk in St A. The fix you need is with train + bus.1 reply 0 retweets 0 likes
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.