Hacker News Reader

Comment by Animats | Hacker News Reader

OK, so you write pre and post conditions for a function, and the function gets generated.

OK, so now we're programming at the specification level. I've written formal specifications for an operating system. They're harder to write than code for non-trivial programs.

Some things are trivial to specify but hard to code. A hash table, for example. It's easy to specify what a hash table does, but that gives no guidance on how to implement one. You might get out something that does a linear search. File systems and databases are similarly not too hard to specify - the specification describes the abstract brute-force approach.

They need to get much further along before announcing victory.

View on HN

You indirectly get at an important point:

A complete specification must include best/worst/anortised performance constraints, and a lot of other details we often leave unstated.

And then it gets a lot harder...

A complete specification also must include assumptions about external systems and limits.

Here the assumptions are infinite stack (or item count < stack size limit) and a malloc that never fails.

Incomplete specs are just as bad as buggy code. I'd even argue that incomplete specs are worse in this scenario, because the "proven correctness" gives a false sense of security.

Performance is not a part of behavior. Specification is about specifying logical behavior and that's it. I don't know of any specification framework that supports saying anything about performance.

This is a very relevant point about program synthesis in general, but if we look at an example given here, the linked_list spatial predicate, the specification is at the much lower level of abstraction of pointers and memory addresses. I would guess that a corresponding specification for a hash table would at least preclude candidate solutions that use linear searching - though there are other ways to make hash tables inefficient, such as a poor hashing function or an inefficient way to handle collisions.

The purpose of this article seems to be to introduce us to separation logic for reasoning about programs with pointers, and in particular the separating conjunct, which "restores compositionality of analysis" (which is lost when spatial assertions assert that some particular property holds over the entire heap.) It goes on to explain that "As it turns out, the compositionality and modularity of separation logic means that it can actually be quite easily adapted to fit into a deductive-reasoning-based automated synthesis strategy."

The title, therefore, should not be read as a claim about the future of programming in general.

In predicate calculus specification languages, you can write

    X such that P(x)

where P is a test predicate. Doesn't mean you have any idea how to generate X. A long time ago, when this idea was going around for the first time, I was using a formal specification language called SPECIAL. I wrote the statement of Fermat's Last Theorem in Special to demonstrate that merely being able to formally specify something doesn't necessarily lead to a solution.

Indeed, but as far as I can tell, the particular specification language here is at a much lower level of abstraction, one where we have only slightly-abstracted pointers, and consequently, I suspect, a specification using this particular logic will have no choice but to say how to generate X (or perhaps I should say that the intention is that one should say how to generate X, even if, formally, one can avoid doing so.)

In programming, coding is a tool for discovering the under-specified parts of the specification.

> Some things are trivial to specify but hard to code. A hash table, for example. It's easy to specify what a hash table does, but that gives no guidance on how to implement one. You might get out something that does a linear search. File systems and databases are similarly not too hard to specify - the specification describes the abstract brute-force approach.

One of the next steps for formally proven software development is automated analysis of algorithms. The same procedure to generate a proof of a correct implementation of a hash table could be extended to take an axiom of randomness (which would be an optimization the metaprogrammer could supply, breaking the true worst-case analysis based on their trust of the hash function and potential adversaries) for the hashing function in order to prove the amortized search/insertion time to be O(1) per element assuming the implementation is free to resize and rehash the table as it grows. The synthesizer could further search for implementations that minimize amortized/average cost using the available axioms and predicates, and benchmark them on a particular architecture much like JIT runtimes do now.

There's just always a "who watches the watcher" recursive paradox with formal specification / verification. Who ensures the specification is a good one?

I believe it is just that - a logical paradox. It cannot be answered. We will always have to be double-checking the specifications, perhaps via model checking.

All that's to say, I agree with you, it's not like this is going to solve all problems just by using formal specs.

>> Some things are trivial to specify but hard to code.

Well, that's the point of automating the coding effort. The specification guides a search for a program that satisfies it. In your hash table example there's no need to tell the synthesiser how to code the hash table, only what the hash table has to do.

The search of course can get very expensive and that's an important bottleneck in program synthesis. But, in principle, if the specification is correct, then a correct program is somewhere in the program search space and a search will eventually find it.

Did I accidentally say something offensive in the above comment?

Just reading the thread now, and the silent downvoters might be objecting to the "eventually" part. "Find the busy beaver program for a 20 state Turing machine" is easy to specify, but could take quadrillions of years to return a result.

Thanks, that could be the reason. But it's also a truism. The only guarantee that can be given for a search procedure is that if a target exists, the search will find it. An infinite search space is an infinite search space and there is no search that can search it in finite time.

Anyway that's the rules of the game for search-based program synthesis. The best that can be done is to guarantee that the search space contains the program. It's an important bottleneck and in my opinion is part of what has kept the field back from fully achieving its goals (which are diverse- and there are diverse sub-fields also).

Reply on news.ycombinator.com