Verified Semantic Versioning

The basic idea of semantic versioning is:

Given a version number MAJOR.MINOR.PATCH, increment the:

• MAJOR version when you make incompatible API changes,
• MINOR version when you add functionality in a backwards-compatible manner, and
• PATCH version when you make backwards-compatible bug fixes.

In a setting where we have verified code, we can also verify correct use of semantic versioning.

Patch release

In a patch release, you proof that all input requirements are equally strong or weaker and all output guarantees are equally strong or stronger. In other words, the new version is a correct implementation of the old specification.

Note. The old version is not necessarily a correct implementation of the new version.

Todo. Or should they be entirely compatible?

Minor release

In a minor release, you do the same as a PATCH release but you are also allowed to extend the specification in ways other than a strengthening/weakening. The overlap still correctly implements the old specification.

Major release

In a major release, you are allowed to overhaul the entire specification.

Note. It can be useful to also release a migration layer that implements the old specification in terms of the new one, if possible. This allows users to automatically migrate.