def foo():
    return True

  def foo():
    return halts("some turing machine program")

Of course, one can still likely get useful answers of "definitely incompatible" etc., with much more tractable analyses. AIUI, the Elm version ends up just looking at the function signature, and catches things like removing or adding arguments: for appropriately restricted languages, it is likely to even be possible to determine if downstream code will still compile, but that's not a guarantee it will behave correctly.

That said, in practice I'm not sure it is too useful (this is a slightly different question to the one originally asked, though). My understanding is the proof of decidability is essentially a pigeonhole principle argument based on LBA having a finite number of states: run the LBA for that many steps, if it hasn't halted, then it has looped. Even if a program is running on a system that only allows programs to use 1GB of memory, there's 2^(2^30*8) (approximately 10^(2.6e9)) states.

If your language lets you build a neverending loop/datastructure/etgc, then you cannot prove halting for all the programs that can be made by the language.

Since such languages exist, then by extension, it applies to computers.

For one, an invariant might be changed syntactically, without actually changing what it is asserting, reducing to exactly my example above: in its simplest form, the contract could go from in(true) to in(halts("...")).

Secondly, an contract could have been made more permissive, e.g. in(x > 1) becoming in(x > 0), or out(y > 0) becoming out(y > 1). Assuming violating a contract is regarded as a programming error (as in, it isn't considered breaking to go from failing an assertion to not failing), these are also non-breaking changes.

Lastly, changing behaviour doesn't necessarily mean changing invariants/contracts.

In practice your time guarantee isn't going to let you produce a sound and complete static analysis that proves the equivalence of two arbitrary (modulo termination guarantees) functions.

In the real world all programs have a timeout set to the time to the heat death of the universe. This hasn't helped us make sound and complete static analysis.

That's a practical distinction I care about that can't be computed.

Having signature compatibility is an important prerequisite, but I think it's possible worse to have code that compiles but does the wrong thing than to have code that doesn't compile (at least it's obvious to the developer that something needs to be fixed, in the latter case).

  Version 1:
  add Int -> Int -> Int
  add x y = x + y

  Version 2:
  add Int -> Int -> Int
  add x y = x * y

Perhaps with some sort of functional extensionality you'd be able to compute compatibility perfectly, but I can't imagine that ever being feasible in practice.

That being said, what Elm does offer is still a huge improvement over humans trying to guess whether they made any breaking changes :)

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

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.

A bug fix is a change. A breaking change is a change that breaks the API. Doesn't matter if the previous status was the intended one or not.

SemVer not working is almost entirely people simply not following it correctly. The projects that follow it as best as they can have very few mistakes were "woops that was a major change" occurs while projects that use it as a guideline may as well not be using it at all.

Often, there are ways to work around bugs in an API. And, just as often, those workarounds will break as soon as the bug is fixed. The API developer is in a particularly poor place to judge whether a bug fix is breaking or not. Sometimes, they can talk to users to see if a change will break their code, but other times they can't. Thus, it comes down to how well a developer can predict whether a fix will break projects in the wild.

No, it isn't. The most relevant question is "can somebody be using the current API". It doesn't matter if your current API matches the documentation, what matters is whether your current API is out there for others to build on.

Don't try to use a crystal ball or other form of divination to predict what your downstream users have been doing with the code; you will always lose. Instead, suck it up, acknowledge the mistake, and signal the breaking change by bumping the major version.

Maybe next time your developers will spend more time validating their public contract, so they won't have to endure the embarrassment of a major version bump.

Semver both acknowledges and is predicated upon the fact that every bug fix has a range of possible impacts. At one end, some bug fixes have almost no chance of breaking an application. At the other end, some bug fixes will almost certainly break applications.

This is not divination. It is understanding your application and its users.

Finally, in regards to your last paragraph, I genuinely hope that you don't speak to developers like that. Mistakes will always happen. Have a little bit of respect and treat people with kindness.

Yes. That's exactly how SemVer works. It signals to people that there was a breaking API change - it doesn't matter if you're on version 10495.0.3 - if you've somehow broken your API 10,494 times you're following SemVer. Although if you're that bad at maintaining a stable API you probably don't have any users you know... using it.

SemVer is predicated upon the fact that other people are using your API. It signals to them whether or not it should be safe to update without breaking their code that relies on your API. If you break your API - you broke their code. That makes you an asshole in their eyes. The entire point of SemVer is to signal that you broke your API so that people relying on it can examine their code for breakage, decide whether or not to update, or start working on modifying their code to match the new API.

If your API is very unstable then people aren't going to rely on it. If it's both unstable and you don't signal breaking changes I'd be amazed if anyone put up with working with it.

If I'm using version 3.0.2 I should be fine using any 3.y.z version. If you release a 4.0.0 then I know I need to investigate and determine whether or not it is safe for me to update to that version. If your API is still unstable and changing on a daily basis - you shouldn't be at 1.0.0 yet. 1.0.0 is meant to signal the "stable API stage" of development.

Doesn't matter if it breaks it in a way that you don't expect users to have been using it - you broke it. Doesn't matter if you were just fixing a typo that changed behavior - you broke it. Doesn't matter if you were fixing a logical error - you broke it. Doesn't matter if you fixed the PRNG causing some results to no longer be possible - you broke it. Doesn't matter if you deleted a deprecated endpoint - you broke it. '

SemVer isn't asking why you broke it - it's asking did you break it.

But behavior testing is undecidable, easily follows from halting theorem. I doubt it would even be recognizable.