> Major flaws in a specification for one function are usually quickly picked up when the proof for another function relies on the missing specification properties

Great point!

> supplementing with standard e.g. unit tests helps catch specification bugs like this

I don't think it does -- any specific input+output pair that a unit test tests for will satisfy all the constraints of a complete spec, so it will necessarily also satisfy an incomplete spec (i.e., a subset of those constraints). You could detect overly strong spec constraints this way, but not insufficiently strong ones.

▲

IanCal 3 days ago | parent [-]

I think you’re picturing the unit test case the opposite way around to me, but what I see relies on having something generated for you. While a unit test case will also pass the weak specs, there exist spec meeting implementations that don’t pass the test.

So either that requires “generate valid code and let’s test it” or that you can write a proof statement like:

If : there is at least one implementation which is valid for the following properties, and does not meet this single property (fixed input output pair) - specifications are under defined.

	▲	akoboldfrying 3 days ago \| parent [-]
		> there exist spec meeting implementations that don’t pass the test. Ah, I see what you mean. Yes, in practice you would have an actual implementation, and if it failed the test but passed the spec you would know the spec was underspecified. I stand corrected. > If : there is at least one implementation which is valid for the following properties, and does not meet this single property (fixed input output pair) - specifications are under defined. Clever! But I guess we're probably some way from being able to existentially quantify over all possible implementations... It might be that the only satisfying implementation is one for which we cannot even prove termination. More optimistically, maybe it turns out that whenever there is a satisfying implementation, there must be one in some simple class (like straight-line programs) that can be checked exhaustively.