3 ms·

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

by rocqua 2y ago

LegionMammal978 2y ago
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!)
- schoen 2y ago
  Huh, this is kind of like other trivial objects in mathematics (typically the empty object and the universal object). One trivial property is "this program computes what this program computes" while the other trivial property is probably "this program computes something". Although these are themselves only trivial in a programming language in which every string represents a valid program.
- not2b 2y ago
  There are other ways to exploit formal verification. For example, you may be able to formally prove that the unoptimized version of your program has the same behavior as the optimized version, subject to specified constraints. This can assure that there aren't any bugs in the optimization that affect program correctness. You're eliminating a class of bugs. Of course, it's possible that the unoptimized version is incorrect, but at least you can assure that your aggressive optimization approach didn't cause breakage. Such approaches are commonly used for hardware verification.
- pegasus 2y ago
  The program includes a lot of incidental complexity which would not be part of the spec. For example, for a sort function, the spec would be the "array sorted" postcondition. The code OTOH could be arbitrarely complex.
  - zozbot234 2y ago
    To be clear, the proper postcondition for a sort function is "the output array is a permutation of the input array and it is sorted".
e2021 2y ago
how do you know the specification is correct? Its turtles all the way down here

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

by rocqua 2y ago

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

LegionMammal978 2y ago

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!)

schoen 2y ago
Huh, this is kind of like other trivial objects in mathematics (typically the empty object and the universal object). One trivial property is "this program computes what this program computes" while the other trivial property is probably "this program computes something". Although these are themselves only trivial in a programming language in which every string represents a valid program.
not2b 2y ago
There are other ways to exploit formal verification. For example, you may be able to formally prove that the unoptimized version of your program has the same behavior as the optimized version, subject to specified constraints. This can assure that there aren't any bugs in the optimization that affect program correctness. You're eliminating a class of bugs. Of course, it's possible that the unoptimized version is incorrect, but at least you can assure that your aggressive optimization approach didn't cause breakage. Such approaches are commonly used for hardware verification.
pegasus 2y ago
The program includes a lot of incidental complexity which would not be part of the spec. For example, for a sort function, the spec would be the "array sorted" postcondition. The code OTOH could be arbitrarely complex.
- zozbot234 2y ago
  To be clear, the proper postcondition for a sort function is "the output array is a permutation of the input array and it is sorted".

e2021 2y ago

how do you know the specification is correct? Its turtles all the way down here