Comment by seanwilson | Hacker News Reader

Comment by seanwilson | Hacker News Reader

Parent Full thread

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 e.g. if you only prove the list returned by a function has a certain length and nothing about the contents of the list, you're going to quickly find out when another function needs to prove anything trivial about the contents of that list.

Not that it's flawless either, but supplementing with standard e.g. unit tests helps catch specification bugs like this and you could generate unit test examples from the specification to review for correctness as well. You would notice problems when running the program too just like with regular programming, you wouldn't just write proofs about your program and not try running it.

Nothing is perfect but just like in regular programming languages where adding a few simple regular automated tests or some more accurate static type annotations (e.g. JavaScript to TypeScript) will catch a lot of problems compared to nothing at all (and with diminishing returns), a proof of some simple properties will flush out a lot of bugs and edge cases. So I feel the common reaction of "specifications can have flaws" is overplayed when it's clearly a big step up the process of eliminating bugs.

Does an alternative exist that's foolproof?

> 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! In a sense, it's testing by immediate use at compile time. I always imagine this to be the greatest productivity booster, even greater than AI. You'll notice things are wrong as you type.

> 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.

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.

> 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.

Reply on news.ycombinator.com