| You certainly cannot determine that two programs do or do not have the same behaviour in the general case. In specific cases, the proofs can be pretty trivial: https://tinyurl.com/ycx2245q - proof your two programs are different https://tinyurl.com/y7lcv3re - proof 'y + x' is the same as Version 1. These proofs weren't automatically discovered, though for such simple programs I'd expect an SMT solver to be able to find the proof or a counterexample easily enough. But even proving they're the same value for all inputs isn't all that helpful, because of lazy Haskell code like: version 1:
fib :: Int -> Int
fib n = if n < 3 then 1 else fib (n - 2) + fib (n - 1)
version 2:
fib :: Int -> Int
fib n = let fs = 1:1:zipWith (+) fs (tail fs) in fs !! n
They're (provably) the same for all (positive) input values, but if you call version 1 with n greater than, say, 35, you'll be waiting quite a while for an answer, while version 2 will be very snappy for the first few hundred thousand values of n, at least, after which the size of the answer will be a bottleneck.If a library switched from the latter to the former, it'd have a good chance of breaking code. While obviously exponential code is obviously exponential, this sort of behavioural change can show up in less obvious ways - a change in memory usage might blow your heap after a supposedly minor version change, eg. In the end I don't think the value judgement of 'breaking' or even 'significant' is computable, and you'd need to rely on a human doing something that approximates to 'right' for your world view with their version numbering. |