Why do tests and types work ?

NOTE HXA7241 2016-01-17T13:06Z

Some epistemology of software correctness – the underlying method seems to be repetition.

“Is it not obvious? You write the test, and if it fails, you know the software is incorrect. (And ultimately similarly for types.).”

But how do you know the test is correct? If the test fails, how do you know that the original software is not right, and the test is wrong? The problem is that neither has authority over the other. And ultimately similarly for types, in their specification and use.

There are sayings about types: that they ‘make incorrect states inexpressible’, or that they ‘ensure the software is correct by construction’. Both these must be wrong – they both beg the question. For the first, how do you know the types are not making the correct states inexpressible – as the earlier point about authority? Merely making some arbitrary states inexpressible – what is the value in that? – In fact the main problem in type research is making type-systems express more. For the second saying, it is doubly wrong: as just explained, but also the software is clearly not guaranteed correct by construction, because the type-system finds errors in it.

One might well now choose to moderate the claim, to be that types and tests ensure consistency rather than correctness, but it still does not answer the question – it simply jettisons the matter of correctness. But it is some way toward answering.

If what we have is, in the end, all just code, all from the same source of information, how does calling some of it tests, or type specs – whatever might be done with them – how does it help with correctness? It seems a lifting-by-bootstraps situation.

————

The answer to how tests and types work is this: they force repetition of expression of intention, and refer discrepancy to human judgement. Consistency is part of this, but you have to have the repetition and the judgement.

It is like setting a password: you are asked to repeat it.

This helps correctness because the ultimate authority is our intent, and there is some reliability in our expressions of it: our expressions are neither perfectly faithful – we would not need the help of tests/types, nor entirely noise – nothing would help. Redundancy, of repetition, reduces the chances of erroneous expression, presumably by something approximating the product of probabilities.

————

(Is not the physical neuronal changes in the brain an objective reference for personal memory, for knowledge? (Re: Wittgenstein, Zettel: §650 §657p1 §659 §660.). I.e. feeling sure really is worth something.

To say we need objective reference is to say we cannot ever rely on feelings of sureness, we must always check every detail. But that cannot be. Our subjectivity depends on us having something not fixed to the objective, and something substantial. If every detail of our knowledge must be checked, our knowledge has no independence – so we must have none. But this is false: we do have independence, so our knowledge must have some reliability.).

————

But when you set a password, could you not have a system where you have previously set a password type, and your new password is checked against that? That is not using repetition. Types seem to work a different way.

Do not types factor the specification, the expression of intention, into one place? Where is the repetition? Well, the type specification, and all the uses of the type, are the two repetitions, but of a different, more complex, kind. But does not the spec have authority, and the mistakes in usage are overruled automatically? No. The errors are always brought to attention. Consider an example: the type for some widely-used data was defined as an int, but a function is then made that is found actually needs a float to do the calculation properly. You realise you made a design mistake: the data type really needs to be a float after all. So anything expressed in the type spec can be brought into question and overruled by usage of the type, so spec and use, though they have different forms, are indeed full repetitions of intention.

————

But tests and types are different, are they not? Are not types better, more powerful? Yes: because types leverage abstraction – this is the more complex kind of repetition they embody. Making a type is something like specifying a whole set of tests at once.

But (notwithstanding this more complex mechanism) this leverage still only works on the grounds explained before. It works as a form of making the programmer repeat their expressions of intention, and making the programmer check what they want.

————

Related: