So, most software depends upon third-party libraries, to some extent or another. Specifications of such libraries' behaviour usually takes the form of human-readable documentation.

We write integration tests to ensure that interactions between our software and these libraries yield the expected behaviour.

But suppose instead that package maintainers published some formal (machine-readable) specification of the contract to which their library's API adheres:

  • repositories could enforce semantic versioning by comparing changes in specification

  • repositories could reject packages that fail automated verification against their specification

  • users of those repositories could be comfortable that the library adheres to its specification, modulo trust of the repository's automated verification process (but could also perform automated verification of their own)

  • users of the libraries could automatically have test stubs generated from the specification

  • (some) integration tests may no longer be required

These all seem like pretty big wins to me. Yet I don't see any package management tools or repositories doing anything like this.

What am I missing?

  • 1
    I guess you are misinformed, there are several module systems which provide formally, machine readable contracts.Which programming language eco systems / module systems do you have in mind? – Doc Brown May 12 at 13:40
  • 4
    I suspect that, like most things that aren't done in software development, this one isn't done because it's simply not worth the additional time and effort it would require. There is such a thing as "good enough." – Robert Harvey May 12 at 13:53
  • 1
    Speaking as a maintainer of some NPM and PyPI packages: because I don't know how to and, from what I've seen for even simple methods, formal verification would take an order or so of magnitude more effort than the writing of the actual code did. Automated testing gives me enough confidence with far less work. – jonrsharpe May 12 at 13:57
  • 1
    @DocBrown then as a maintainer of some NPM and PyPI packages it's because I don't really know what that is, apparently! – jonrsharpe May 12 at 14:02
  • 1
    ... note that in compiled languages like Rust, you usually get formal signature violations signalled pretty early once you start using a package and try to compile it together with the using code. This is often "good enough" for most people, as @RobertHarvey wrote above. – Doc Brown May 12 at 14:22

What am I missing? ... I mostly had JavaScript/npm and Rust/Cargo

Strong Typing.

| improve this answer | |
  • 2
    @user365547: if you take Haskell, it's not “just signature comparison.” Essentially, it all depends on the tools you use. With Ada or Haskell, the interface is quite strict. In JavaScript, the interface is quite relaxed, because accepting and being able to handle different types is by design. This is the choice the designers of the language made, and both choices make perfect sense. – Arseni Mourzenko May 12 at 15:02
  • 1
    @user365547 sometimes, it does. There is exactly one Haskell function with the type a' -> a' – Caleth May 12 at 15:09
  • 1
    put your unit tests in class constructors. – Ewan May 12 at 15:13
  • 1
    @user365547 Type systems are automated proof checkers. We declare properties about the behaviour of our program such as “this function will only return integers”, then let the computer prove that this is correct. But because running proofs efficiently is very tricky, and because writing automated proofs can be quite hard, the power of those type systems is super restricted (never mind that C++ templates or most trait systems are Turing-complete anyway). Often, the trick for strong proofs is to make values unrepresentable if they are invalid. – amon May 12 at 15:13
  • 1
    But I think you are missing the point. Yes, typing is a limited form of contract, but you are coming from an ecosystem which rejects this kind of control. "does microsoft's signed dll for a .net component in a strongly typed languages functionality match its documentation?" is a question I dont need to ask. "wft does this random npm do?" is a question I ask myself every day – Ewan May 12 at 15:17

What would it take to make good, solid, trustable contracts? The contract would have to be very detailed.

Do you know what we call a contract detailed enough to specify the inputs and outputs of piece of behaviour? Code.

So what are your really asking for here? Two separate and executable implementations.

Lets just assume we did do that...

  • When the contract is satisfied, does it mean there are no errors? nope, the error can be formally specified
  • When the contract is satisfied, does it mean the software performs? nope, bubble sort, and log sort are both stable sorts - very different performance
  • When the contract is violated, do you get compensated? Probably not
  • When the contract is violated, do you get a warm fuzzy feeling that you caught them lying? ... so you are perfect?

So in reality contracts that are sufficient to just be trusted have some issues right out of the gate.

As to your other points:

  • Semantic versioning isn't the only versioning scheme on the planet. That aside its not terribly formal. Does new behaviour imply a minor bump, or is it a major bump? In many languages its minor, but in a language that permits reflection, that is a change in behaviour -> major bump. Unless the client doesn't care about reflection.
  • We already verify builds using test suites. The more complete and expansive the suite the higher our confidence.
  • Which is why integration and end to end test exist. To prove that the library meets our expectations.
  • I seriously doubt any level of testing on the vendor side nullifies testing on the client side. Its still a risk, and its still your risk. It really does not matter how many platitudes are given.
| improve this answer | |
  • I think I overemphasised "specification" in the question more than I'd intended. You will no doubt see from some of my comments that I had really been thinking more about external behaviour tests (which library authors will often have written and be verifying before publishing anyway). If the repo were to guarantee not only that such tests exist and pass but furthermore that those same tests will continue to pass for "compatible" future versions too, then I can review once and have greater confidence than the status quo, where I have to track internal details on every release or test myself. – user365547 May 13 at 8:16
  • @user365547 How often do you have to change tests that guarantee the same behaviour? Honestly when internal behaviours are refactored, the answer is a lot. The only tests that don't change are my integration tests, because they have no internal knowledge, and they are slow... so slow... and woefully incomplete. – Kain0_0 May 13 at 23:08

If they have eggs, get six

What am I missing?

It always reminds me of that old joke:

My wife said: "Please go to the store and buy a carton of milk and if they have eggs, get six." I came back with seven cartons of milk. She said, "why in the hell did you buy seven cartons of milk?"

"They had eggs"

Or, while we're at it:

A programmer goes out to get some dry cleaning. His wife told him, "While you're out, pick up some milk".

He never went home.

Humans have an innate ability to understand context and parse information relative to that context. Machines lack this skill entirely. Machines do what you instruct them to do, and don't care about whether the overall intention of your instructions can be understood or not.

Because of this, when given the exact same text to parse, humans and machines will not always take away the same information from it, and that's the main reason why you can't just define an arbitrary language that explains specifications for all parties involved without any ambiguity.

Arguably, programming languages are already our best attempt at doing so. But machines require such pedantic detail that the resulting language is complex and requires experts trained in reading it (software developers). Developers can't even decide on which programming language we should universally use, let alone that we're going to be able to define a specification language that everyone (including machines) innately understands without requiring a particular skillset or training.

Don't get me wrong, we are definitely streamlining the process. If you compare third-generation languages (C#, Java, ...) to the much older second-generation languages (Assembly), the human readability factor has increased tremendously. But we're not at a point where it maps to plain English, it still requires specialized training. Maybe we'll get there someday, but not right now.

Non-developers generally cannot make heads or tails of modern-day programming languages, and this is the main reason why your proposed specification language cannot exit; because it's those non-developers that make the business decisions and define the specifications that applications should adhere to. Developers are the necessary translation between non-developers and the machine.


My first response to your question was to try and explain that unit/integration testing does exactly what you're asking for. But you mention integration testing yourself, so you must be aware of that.

Unit/integration tests are the tests that are meant to confirm that the library does what its specifications say that it does. All it requires is for a developer to boil these requirements down to actual test code.

I assume the basis of your question is "why do we need to translate specifications to code? Why not write in a way that both humans and machines innately understand?", which I already addressed in the previous section.

One more thing:

Why stop there?

Your question asserts the feasibility of defining a specification language that can be understood by man and machine, without any ambiguity or inconsistency. I've already addressed why that assertion is incorrect, but let's for a second entertain the idea that it were feasible.

Why would you stop at specification testing? If we have this language, then this language can similarly be used to write the application itself, meaning that programming languages would become obsolete, in favor of human-readable specification language which the machine can (allegedly) parse and understand with no issue.

Don't forget that the main purpose of a developer is to be the expert translator who "reads the sacred text" (i.e. the programming language).
The specification language you're proposing is the equivalent of having a translation dictionary between English and the sacred language that is so absolutely perfect that anyone who only speaks English is able to perfectly communicate in the sacred language (and vice versa) without any specialist training.

If that dictionary were to exist, then you no longer need to rely on your sacred translators (i.e. software developers) and you can cut out the middle man entirely.

In short, the specification language you're asserting that can exist is the essence of software development in and of itself.

| improve this answer | |
  • I think I overemphasised "specification" in the question more than I'd intended. You will no doubt see from some of my comments that I had really been thinking more about external behaviour tests (which library authors will often have written and be verifying before publishing anyway). If the repo were to guarantee not only that such tests exist and pass but furthermore that those same tests will continue to pass for "compatible" future versions too, then I can review once and have greater confidence than the status quo, where I have to track internal details on every release or test myself. – user365547 May 13 at 8:19

It all depends on the language, ecosystem and culture.

Take Haskell. You don't need humanly readable documentation to tell you that you need to put a number between zero and one hundred or that you can have a sequence of zero or more elements or nothing in return. You just know that. Your compiler knows that.

Now take JavaScript. Stakes here are different. The choice the designers of the language made originally was to allow any type to be passed to a function, and try to handle it if possible. This is, again, by design, and it is a perfectly valid choice.

In C# and a bunch of other languages, you also have code contracts. Those are pieces of code that tell something about the requirements about the parameters, or about the return values. For instance, if you pass a positive value to parameter x, you will get a non-negative value in return. Those rules are then checked automatically, and if the code violates a contact, an error occurs.

| improve this answer | |
  • But yet we still write tests for Haskell; e.g. to verify that some example inputs produce the expected outputs. This gives us greater confidence in the implementation than type signature alone. Knowing that a Haskell library passes a set of tests, and knowing that the repo will enforce future versions to continue doing so modulo semantic versioning, together with all the other benefits listed in the question... surely still adds something that isn't currently available? – user365547 May 12 at 15:18
  • 1
    What exactly do you want to test, your code or the third party libraries? In the first case, you just need to know the interface of those libraries, and consider the implementation as a contents of a black box. In the second case, you just fork the third party library on GitHub and test it. – Arseni Mourzenko May 12 at 15:31
  • I want to be confident that, if I depend on a library, it does what it claims. Currently I don't know if it passed ANY tests before it was published and I certainly don't know whether future versions will continue to do so. These are things that the repo (an independent trusted entity) could guarantee for me, but it doesn't. Consequently the surface of (my own) code that I (together with every other user of that library) must test is much greater than it need be. – user365547 May 12 at 15:40
  • What repositories are you looking at that don't show you the test results for a given version? – Caleth May 12 at 15:42
  • 1
    @user365547, so the library passes the interface test. How do you know that the interface test is correct and covers all cases that are relevant for your usage of the library and continues to do so for future versions? Are you going to blindly trust the library authors on that? – Bart van Ingen Schenau May 13 at 6:08

What am I missing?

A set of tests, or a formal verification of specification, can tell you that a given function does what it's author intends it to do.

It doesn't help you know whether what it does is equivalent to what you want. You still have to figure that out yourself.

| improve this answer | |
  • But, currently, I don't know if a Rust crate passes ANY tests before it has been published and I don't know that future versions will continue to do so. If the repo only accepts crates that pass a set of tests, and enforces that future versions always will continue doing so (modulo semantic versioning) then I have greater confidence that the crate does what its author claims. Which reduces the amount that I need to test myself. – user365547 May 12 at 15:22
  • And not just me, of course. The issue scales linearly across all the crates users, who are all currently having to test that it is doing what they think. Whereas if they were able to rely on the repo enforcing certain of its claims, the total savings are considerable. – user365547 May 12 at 15:25
  • @user365547 most users of most packages trust that it does what it is documented to do, so no, it's not linear in users. – Caleth May 12 at 15:55

If you have a package repository and you want it to to be successful, then it needs users. To get users it needs to have packages. To get packages you need the barrier to publishing to be as low as possible.

So basically there is no motivation for a repository that wants to be big to add barriers that make publishing more difficult, and if there are repos that have these kinds of barriers, they likely just won't get to the point where they are big enough for the average developer to be aware of them.

| improve this answer | |
  • 1
    This answer seems to gloss over the logical consequence that OP's proposed feature would be desirable for the repository's consumers, which in turn incentivizes publishers to use the feature (and thus repository). This answer presumes that supply must come before demand, but it's more often than not the other way around, where the consumer's demand is what drives the publishers to supply the demand. – Flater May 13 at 8:17
  • While it's true that demand can drive supply, I would argue that here there is no demand. There isn't a repo that has this feature, because there aren't enough people who want this feature to drive that demand. The repo I deal with the most frequently is npm, which I would argue is huge because it has almost no barrier to publishing. When I go there to look for a package, even if I can't find one that is perfect and meets my needs exactly, I may find several that are close, or at least someone that tried, that gives me a better starting point than if I had to build something from scratch. – Jason Kohles May 13 at 22:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.