In the Tau Alpha the discussion is the description of what. Logical relation (x,z) are a proof method. So in this case the formal specification or "model" is solidified as a result of the discussion process. So when Ohad speaks of a million participant discussion where an agreement is reached it simply means that as a result of this discussion some formal specification (WHAT) is defined.
A constructive proof which is produced by deductive theorem proving. The search is: Find a program P that
meets the input/output specification. Deductive synthesis works by 1) complete the specification, construct a graph and apply SAT solver to search this graph, optimal (lowest cost) program P which meets the specification requirements is located. In essence the proof search method to find the optimal program matching the requirements outlined in the specification. This is also semantics preserving.
We don't have to worry about the how directly because the how is derived from the what. The what is the specification and the solver brute force locates the solution P (program). The how is whatever meets the specification at the lowest cost (optimal solution P). The search algorithm is typically combinatoric search over a finite selection of possible proofs. The output is typically the top or best program which satisfies the specification which means the quality of the specification is very important.
