Talk:Program synthesis

	This article is within the scope of WikiProject Computing, a collaborative effort to improve the coverage of computers, computing, and information technology on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.ComputingWikipedia:WikiProject ComputingTemplate:WikiProject ComputingComputing
???	This article has not yet received a rating on Wikipedia's content assessment scale.
???	This article has not yet received a rating on the project's importance scale.

Please discuss the merge at Talk:Automatic programming ---- CharlesGillingham 05:53, 26 August 2007 (UTC)[reply]

Rewrote the article (July 2017)

I am a postdoc at UC Berkeley working on program synthesis User:MarkusRabe. I tried to address some of the problems with the previous version of this article (vagueness, poor writing, missing references, sometimes even wrong statements). I rewrote the introduction, origin, and current developments and I deleted "Problems and limitations" as it used too specific technical terms, such as 'factoring' and was very vague.

From here on, the article should be extended by more detailed discussions on modern algorithms for program synthesis, for example FlashFill by Sumit Gulwani, enumerative program synthesis, component-based synthesis, and so on. The current section on Manna and Waldinger's work is okay, but their approach does not play a big role today. - 4 July 2017‎ User:MarkusRabe

I agree that the Manna+Waldinger section currently has undue weight; it got even longer due to (apparently necessary) additional explanations. I hope this problem will vanish if some people add new sections on other, in particular, more common, approaches. Maybe, we will have to split the article eventually. - Jochen Burghardt (talk) 12:09, 11 February 2019 (UTC)[reply]

Copyright problem removed

Prior content in this article duplicated one or more previously published sources. Copied or closely paraphrased material has been rewritten or removed and must not be restored, unless it is duly released under a compatible license. (For more information, please see "using copyrighted works from others" if you are not the copyright holder of this material, or "donating copyrighted materials" if you are.) For legal reasons, we cannot accept copyrighted text or images borrowed from other web sites or published material; such additions will be deleted. Contributors may use copyrighted publications as a source of information, but not as a source of sentences or phrases. Accordingly, the material may be rewritten, but only if it does not infringe on the copyright of the original or plagiarize from that source. Please see our guideline on non-free text for how to properly implement limited quotations of copyrighted text. Wikipedia takes copyright violations very seriously, and persistent violators will be blocked from editing. While we appreciate contributions, we must require all contributors to understand and comply with these policies. Thank you. Osiris (talk) 13:04, 7 July 2012 (UTC)[reply]

This page needs a complete rewrite

The current contents of this page describe the state of program synthesis prior to 2000 (the only citation is from a 2004 review paper looking back at the eras from 1960-2000).

I am postdoc at UC Berkeley with primary research focus on Program Synthesis. My PhD was on Program Synthesis as well. I am starting on a project to revamp this page to make it current with the developments in the field, and I will ensure that the updated page contains contributions from faculty and researchers at all prominent establishments (including Berkeley, MIT, Microsoft, etc.) working in the area. The end result will bring the page up to par with, for example, the Software testing page.

If any of the current contributors have significant objections to a rewrite, please respond. — Preceding unsigned comment added by Saurabh.berkeley (talk • contribs) 19:28, 23 April 2013 (UTC)[reply]

Other aspects of program synthesis

This page only considers program synthesis from formal specification,e.g., LTL or CTL temporal logic. The important topic of program synthesis from input/output examples is omitted. Currently, the later is more actively pursued and has been already transferred to the industry, e.g, MS Excel's FlashFill feature. I refer here to the recent and remarkable works of Sumit Gulwani of MSR. — Preceding unsigned comment added by 131.246.78.12 (talk) 07:36, 14 July 2016 (UTC)[reply]

Confusing example

The "toy example" is very hard to read and understand for non-math people (including software engineers like me). Obvious questions to start:

"The maximum is larger than any given number, and is one of the given numbers" sounds to me like an impossibility. Is that a mistake or poorly phrased or what?
What does the axiom "A=A" mean in words and why is it required?

-- Beland (talk) 06:06, 28 May 2016 (UTC)[reply]

The informal specification of maximum was sloppy; I fixed this (not quite sure whether "larger or equal than" is ok or "... to").

"A=A" is the reflexivity property of equality; the remaining axioms aren't used in this example, so I omitted them. Reflexivity is used to obtain line 14 from line 12; informally, the (trivial) equation "x=M" (with x a constant and M a variable) is solved w.r.t. M by resolution with "A=A". - Jochen Burghardt (talk) 17:07, 28 May 2016 (UTC)[reply]

@Jochen Burghardt: Your rewrite clarified these questions, and I've removed the {{confusing}} tag. Thanks a bunch for your work on this article! -- Beland (talk) 17:43, 15 February 2019 (UTC)[reply]

The example at best produces only expressions that utilize only the ?: 3-place Boolean function. Even using this function more than once e.g. x?y:(z?w:v) would not be possible without a reference to how parentheses are generated. The work of Volkstorf cited describes the creation of complete PHP programs, which is vastly more complete than this example, but is given an only cursory mention. — Preceding unsigned comment added by 2601:184:4081:1CBE:BCCD:9145:66F5:A63E (talk) 04:46, 9 February 2019 (UTC)[reply]

In-text critics by anonymous user

CRITIQUE: Program Synthesis means creating a computer program from scratch, not plucking one from a list of one. You can only produce that one program. Surely a system for creating computer programs that constantly is unable to produce anything until once in a blue moon someone asks for that one program, is not an example of how computer programs can be constructed automatically. It should either be removed or admit that it produces only one program and isn't really program synthesis.

A better way to produce that result is by having a program ask "Do you want a program to take the maximum of 2 numbers?" and if the answer is yes it outputs that program, and if the answer is no it says "Sorry, no can do."

 — Preceding unsigned comment added by 2601:184:4081:1CBE:EC4B:754:77D:69F5 (talk) 21:20, 25 August 2019 (UTC)[reply]

I insert here paragraphs that were inserted into the article by an anonymous user. While they are valuable for the improvement of the article, they don't belong there. - Jochen Burghardt (talk) 09:01, 11 February 2019 (UTC)[reply]

This gives the steps in a proof and then presents a programming language expression. However, there is no explanation as to how the expression was derived from the proof. The expression contains variables and symbols ? and : but there is no procedure given for constructing an expression consisting of these characters.

26 January 2019 - 2601:184:4081:1cbe:8c24:e846:2c8e:12f8

However, there is no rule or procedure described that explains how or why the question mark and colon characters are introduced in line 58, in which the string p ? s : t appears. Furthermore, there is no explanation as to how programs which consist of commands such as assignment, if-else or loops are created.

9 February 2019 - 2601:184:4081:1cbe:bccd:9145:66f5:a63e:L

However, the example does not follow the form of logic and resolution in particular. Wiki resolution states: “produces a new clause implied by two clauses containing complementary literals” e.g. “avb, ~avc => bvc”. 14 Resolve(12,1) uses 1 and 12 but they are not of the form avb and do not contain complementary literals. Likewise for 15, 17, 18. 16 is derived from 3 and 15, but if y=x then 15 is true but 16 is false. 16 contradicts 15. Lastly, 19 derives x<y ? y : x from contradictory statements x <= y and ~(x <= y). If this is Resolution then we would derive false. There is no explanation as to what in general is derived e.g. if we have x=y and ~(x=y) what expression do we derive? In general, from expressions P and ~P what do we derive?

10 February 2019 - 2601:184:4081:1cbe:980f:4a3c:27ed:8bf1

Correction: See Critiques of e.g. Law_of_excluded_middle, Falsifiability, Principia_Mathematica, Zermelo–Fraenkel_set_theory — Preceding unsigned comment added by 2601:184:4081:1CBE:80AC:29DF:4AA7:416D (talk) 17:56, 11 February 2019 (UTC)[reply]

Technical contributions need to be adjudicated or accepted without comment.

11 February 2019‎ 2601:184:4081:1cbe:80ac:29df:4aa7:416d

Ok, "critiques" (let alone "critics", I just found the subtle difference in my dictionary) wasn't the right word - sorry for that! What I meant was this:

Your phrase "there is no explanation of ..." refers to a drawback of the presentation, not necessarily of the contents itself. I am currently trying to improve the former. The talk page here is intended to discuss presentation issues. -

I think your issues of 26 Jan and 9 Feb are resolved in the current article version, aren't they? I guess your issue of 10 Feb is still unresolved; however, I have no idea how to explain it better than referring to the table showing the (non-clausal) resolution rules. - Jochen Burghardt (talk) 09:13, 12 February 2019 (UTC)[reply]