3 ms·

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

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.

Animats 5y ago
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.
- mannykannot 5y ago
  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.)

Animats 5y ago

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.

mannykannot 5y ago
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.)