Comment Comment by bananaflag > Real-world systems are too messy to be specifiedI agree with this counterargument.I mean, you can verify that Euclid's algorithm computes the GCD. Or that quicksort produces a sorted version of the input array.But how do you verify Facebook? Facebook computes what?For some programs, the shortest descriptions of what they do are the programs themselves.Edit: I agree with the replies that you can verify individual parts and properties, like with testing. parent bananaflag 2 months ago
I agree with this counterargument.
I mean, you can verify that Euclid's algorithm computes the GCD. Or that quicksort produces a sorted version of the input array.
But how do you verify Facebook? Facebook computes what?
For some programs, the shortest descriptions of what they do are the programs themselves.
Edit: I agree with the replies that you can verify individual parts and properties, like with testing.