Talk:Program synthesis

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

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)

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)

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)

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)

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)

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)

@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)

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)

Correct Location for Example

To recap the above discussion: In Program Synthesis, 2017 (text available online), Gulwani, Polozov and Singh write, “Program synthesis is the task of automatically finding a program in the underlying programming language that satisfies the user intent expressed in the form of some specification.” Do you agree? If yes, then does the example meet this definition? If it does not, then why call it an “example” of Program Synthesis? If what these authors describe is not Program Synthesis, then what is the correct term for what they are describing and where on Wikipedia is that subject covered?

If your procedure is a manual system for producing computer programs rather than an automated one, then you are describing a Programming Language or, more generally, an Integrated Development Environment (IDE) and it needs to be moved to that page in Wikipedia.

Thanks.

M. Davis

Mdaviscs (talk) 11:53, 15 April 2020 (UTC)

We already have discussed this on 16 Sep 2019. Unlike Gulwani et al., most authors use "program synthesis" also for non-automatic approaches, and insist on a formal specification. Moreover, from an anonymous contribution of 14 July 2016 on this talk page, it seems that their approach is concerned with generating programs from input/output examples, which does not fit here (see Programming by demonstration, Programming by example, Inductive programming, etc. for this). See also the definition in the article's lead. - Jochen Burghardt (talk) 15:34, 15 April 2020 (UTC)

This is not a case of automated vs manual. It is a matter of there being a way to create the program or not.

1. If there is an automatic procedure for creating the program, then you enter the specification and software outputs the program. a. You can show the software and explain how it works - the program construction method.

2. If there is a manual procedure, you go through that procedure and describe in English how you construct a program from the specification, each step in the process.

3. You’re not doing either. You don’t have software to produce it (actual Program Synthesis) and you don’t show a manual procedure for creating the program. You just show a printout of some “rules” and a program. Where did that program come from? Someone wrote it just like every programmer writes programs.

The “procedure” that you describe just leads you down a path from the specification to the line that contains the program that a programmer wrote. It’s not a procedure for constructing a program. It’s a procedure to lead you to a program that was already written by a programmer for this one specification.

You set this up with one (specification,program) pair. You are only feeding that one program to the user and the user MUST request that program. The user doesn’t even have the freedom to request anything else!

So naturally you just write the program in advance because the user is only allowed to enter that one specification. Even if you added more rules, you are still only feeding the user prewritten programs that are the ONLY ones they can request. No programs are constructed. They are written by a programmer in advance for the specifications that the user must choose from - really just a multiple choice.

M. Davis Mdaviscs (talk) 15:36, 4 May 2020 (UTC)

ALSO NOTE:

1. Use of “program synthesis" for non-automatic approaches: Researchers uniformly refer to the process as being “automatic” or “mechanized”:

1. “automatically finding a program that satisfies the user specification” 2. “automatically generating programs from specifications” 3. “automatically synthesizing programs” 4. “computers write programs automatically” 5. “mechanized construction of software” 6. “the problem of generating automatic code” 7. “automatically generating programs from specifications”

 (See references below.)

If you are going to include a manual procedure, then you need to explicitly indicate that it is a manual procedure to distinguish it from the common definition of Program Synthesis.

2. The definition in the article's lead is: “the task to construct a program that provably satisfies a given high-level formal specification.” However, as the program produced is taken from a table contained in the system, the program was already constructed before the user entered their specification. Where does the set of rules come from - is that automated? If a person must create the rules, then the system doesn’t construct any programs. In what sense is a program being constructed when it already existed and it had to be constructed by a person (rather than the system) beforehand?

If I handed you a list of 5 computer programs with their specifications, and said you can find some useful programs there, would that be a program synthesis system? Certainly not. But how is your exercise any different - other than being more difficult to use than my list of programs?

Sources of definitions of Program Synthesis:

1. Program Synthesis - Sumit Gulwani et al. 2. Program Synthesis in AI - Jun Wu 3. Program Synthesis using Abstraction Refinement - Xinyu Wang et al. 4. Program Synthesis Explained - James Bornholt, University of Texas 5. Program Synthesis: Challenges and Opportunities - Cristina David et al. 6. Automatic Program Synthesis of Long Programs - Amit Zohar1 at al. 7. Program Synthesis is Possible - Adrian Sampson, Cornell University

Thanks.

M. Davis Mdaviscs (talk) 22:38, 15 April 2020 (UTC)

In-text critics by anonymous user

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)

• 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)

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)

Another In-text critics by anonymous user

CRITIQUE: The Toy Example given produces only the one program given in the rules. Program Synthesis means creating a computer program from scratch, not plucking one from a list of one. 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)

The Manna-Waldinger approach is able to produce different algorithms even for the simple toy example "maximum of two numbers", if different logical derivations are used for synthesis. For example, int max(int x,int y) { return min(x,y)+abs(x-y); } may well be derived, given appropriate formal properties of min, abs, +, and -. In the Manna-Waldinger approach, there is no list to pluck programs from; I wonder where in the article you took that idea from. - Jochen Burghardt (talk) 08:41, 26 August 2019 (UTC)

Answer for Jochen Burghardt: The Toy Example uses rules that include the only program that can be "created". You are simply telling the system the program to output in the rules. True program synthesis has a mechanism for constructing programs. The example has only the single program that can be produced from the list of one program. - 6 Sep 2019‎ 2601:184:4081:1cbe:b170:ce3:5935:8557

Please: (1) don't change the old text of a discussion, in order to keep it transparent to all readers. (2) Sign your posts, for the very same reason.

The toy example shows only those axioms and rules that are needed to derive it. I guess, Zohar Manna and Richard Waldinger had in mind a large collection of axioms and rules to choose from. Also note that the system is far from being automatic; instead it provided rules to be applied by hand; it does guarantee, however, that the program finally obtained satisfies the specification you started from. Moreover, feel free to add text about other approaches to ("true") program synthesis. - Jochen Burghardt (talk) 15:36, 8 September 2019 (UTC)

Answer for Jochen Burghardt: The definition given for program synthesis is "the task to automatically construct a program". The program "synthesized" is input by a person in line 58. That is not automatic. Furthermore, as you say, "it does guarantee, however, that the program finally obtained satisfies the specification.". That is not program synthesis, that is program verification. Do you really believe this meets the definition for program synthesis given in the first sentence of this article? — Preceding unsigned comment added by 2601:184:4081:1CBE:6862:FA93:3A9:C677 (talk) 15:42, 9 September 2019 (UTC)

I see your point. However, I think that definition is too restrictive: the cited reference, Basin et al 2004, defines in the 1st sentence of the introduction "Program synthesis is concerned with the following question: Given a not necessarily executable specification, how can an executable program satisfying the specification be developed?" (no mention of automatization). On the next page, they say "The objective of program synthesis is to develop methods and tools to mechanize or automate (part of) this process"; "program synthesis" here apparently refers to the research field, not to a tool or method (the latter don't "develop methods and tools"). Indeed, it is the ultimate objective of this field to come up with automatic tools; however many early approaches' contributions were focussed on other subtopics (such as relating to predicate logic as a specification language). I checked one of the references Basin et al refer to for a description of major achievements, viz. [26] (Yves Deville and Kung-Kiu Lau (May–Jul 1994). "Logic program synthesis". Journal of Logic Programming. 19–20: 321–350.), it gives almost the same definition in its abstract (again no mention of automatization), and cites, on p.328, Manna.Waldinger.1980 (=[93]) as a "program synthesis system". This agrees with Manna's and Waldinger's own terminology (see their title).

The difference program synthesis vs. verification is not automatization vs. non-automatization, but whether the program is obtained as output of the method or has to be given as its input.

In any case, you should stop inserting discussion text into the article. - Jochen Burghardt (talk) 15:54, 16 September 2019 (UTC)

In the Toy Example, the program produced is entered by the user in line 58. This is not program synthesis, which is defined on this page as automatically constructing the program. The Toy Example needs to be moved to the Formal verification page listed below. If this is not corrected, this error will have to become a critique.

“It is the ultimate objective of this field to come up with automatic tools; however many early approaches' contributions were focussed on other subtopics (such as relating to predicate logic as a specification language).” The design of the specification language is necessary whether your methods are automated or not.

Critiques are common in Wikipedia.

“I think that definition is too restrictive”: Then it needs to be corrected to match the text of the page. - 17 September 2019‎ 2601:184:4081:1cbe:3d34:2e95:afb4:f746

The program is not entered by the user; line 58 is an instance of the rule in line 19; the "(?:)" operator originates from that rule.

"The design of the specification language is necessary whether your methods are automated or not." — That what I say; and for this reason, I (and, as far as I know, everyone in the community) consider Manna's and Waldinger's approach to belong to the research field of program synthesis, although their approach is not yet automatized.

Debates to settle different opions of editors are to be located at talk pages.

I agree the lead should be changed (as I said, you have a point there), but I wanted to wait for your response before. Would you be ok with the above-cited sentence from basin et al ("Program synthesis is concerned with the following question: Given a not necessarily executable specification, how can an executable program satisfying the specification be developed?"), or a slight rephrasing to avoid copyright problems?

By the way: undoubtedly, there are many more, and better, approaches to program synthesis than Manna's and Waldinger's (which is pretty old pioneering work). Currently, the latter has undue weight in this article. I still hope some other editors will contribute about other approaches in the future, in order to balance the weight. As a short-term measure, one might start an almost empty section for every major approach (found e.g. in the paper by Deville and Lau), and include a tag that it should be expanded. - Jochen Burghardt (talk) 09:42, 18 September 2019 (UTC)

PS: As an analogy in program verification, work has started there with the Hoare calculus, which was pioneering despite its complete lack of automatization; mordern approaches like e.g. Frama-C are fully automatic, and based on Hoare's work. - Jochen Burghardt (talk) 09:46, 18 September 2019 (UTC)

 Done I fixed the lead according to the above discussion. - Jochen Burghardt (talk) 15:48, 24 September 2019 (UTC)

Example Does Not Create an Entire Program

This only produces the one operator p ? s : t with substitution for p, s, t. It does not create any other aspects of a program, such other operators, complete expressions and commands such as assignment, conditional execution and loops. It is not a complete program. This can better be described as “creating a single operator” than creating a program. It is no more program synthesis that building a wheel is building a car. This fact is being suppressed by the author of this page without addressing it. — Preceding unsigned comment added by 2601:184:4081:1CBE:C193:3D85:27BF:92C2 (talk) 15:59, 4 November 2019 (UTC)

As noted in the article, the supported language is Turing-complete. This means that every possible program can be expressed in that language.

The example states "Since the goal formula true has been derived, the proof is done, and the program column of the "true" line contains the program." This is just an expression and programming languages require a lot more than single expressions to be Turing complete. At a minimum there needs to be some sort of looping mechanism e.g. FOR/WHILE/UNTIL. At best (if the proof were correct) you are verifying a single expression (that given in the rules) meets a given specification. It is not program synthesis and it is not even program verification. Perhaps you can call it expression verification. As such it does not belong on this page.

As noted in the footnote nearby, arbitrary new operators and relations can be added by providing their properties as axioms. To keep the toy example in toy size, only ≤ has been (incompletely) axiomatized there. (I now marked footnotes containing explanations, rather than just references, by "note".)

Adding more expressions does not change the fact that you are not synthesizing programs nor even verifying programs.

As noted under "structural induction", e.g. a algorithm to compute quotient and remainder of two given integers is synthesized in Manna, Waldinger (1980), p.108-111. More examples have been published in journal articles; as a reaction to your repeated criticism, I'll look them up and add their references. - However, this will still increase the undue weight of the Manna/Waldinger approach in this article. - Jochen Burghardt (talk) 09:05, 5 March 2020 (UTC)

Semi-protected edit request on 6 March 2020

In the example:

1. Step 16 is not true. x and y are free variables. x and y can be equal, so that both y <= x (15) and x <= y (the negation of 16) are actually true. This occurs when the two arguments to the program are equal. Axiom 3 is not an exclusive OR. (15) is not the negation of either disjunct of (3) and Resolution does not apply.

2. Step 19 is inconsistent with the other steps. The goal, true, in step 19 is the disjunction (OR) of the two arguments, x <= y (18) and ~(x <= y) (16). In the other steps, we are correctly assuming the conjunction (AND) of the two arguments, which would make Goal 19 false instead of true. For example, in 15 we are using the truth of A <= A (Axiom 2), substituting x for A to get x <= x and removing x <= x from x <=x ^ y <=x (14) to get y <= x (15). Certainly axioms are always true.

3. What happens if the input specification is not the maximum of two numbers? Does every program created have to be listed in the Program column of some rule? Wouldn’t that mean that every program that can be created must be supplied in the rules? If that is the case, then why not simply list the programs and their specifications, and compare the input specification to find its program? That would eliminate all of the effort required by the user to locate the correct program. In “A Survey and a Categorization Scheme of Automatic Programming Systems”, Generative and Component-Based Software Engineering, 1999, pp. 1-15, [e.g. https://link.springer.com/chapter/10.1007/3-540-40048-6_1] Wolfgang Goebl notes “All of the program code produced should be generated without the help of the user. All of these so called ‘Automatic Programming’ techniques are very different from the idealistic.” [pg. 2] Simply listing the programs and specifications to be looked up would meet this criteria. Mdaviscs (talk) 16:55, 6 March 2020 (UTC)

Reply:

The section in question presents one approach to program synthesis along published journal articles. I can't help if you don't like the approach. I'm tired of defending it. As for the challenged lines I'm sure they are OK:

1. Line 16 is obtained by resolving lines 15 and 3, according to the rule in line 57, using "y≤x" as p. Manna and Waldinger have proved the soundness of their calculus. Intuitively, the resolution argument at that point can be read: "To prove y≤x, when it is known that A≤B ∨ B≤A holds for all A,B, it is sufficient to prove ¬(x≤y).". (Also note that variables are denoted by capital letters here; x,y are both constants, obtained from reverse Skolemization. Maybe this should be elaborated in more detail in the article?)
2. Line 19 is obtained from 18 and 16 in a similar way by application of the non-clausal resolution rule from line 58, using "x≤y" as p.
3. See #Example Does Not Create an Entire Program. Make sure you understand what a functional programming language is, and what Turing complete means. - Jochen Burghardt (talk) 18:25, 6 March 2020 (UTC)

@Mdaviscs: Please sign all your posts here; it helps other readers to understand the discussion.

As for loop constructs, please note that the approach is able to generate recursive programs (w.r.t. arbitrary well-founded induction orderings), as demonstrated in the quotient remainder example in Manna.Waldinger.1980. This makes it Turing-complete. - Jochen Burghardt (talk) 19:26, 6 March 2020 (UTC)

Simply Put:

1. In Program Synthesis, computer programs are constructed using a formal systematic procedure (algorithm) that a computer can carry out, rather than by a programmer using his particular skills. You correctly state, “the program is to be constructed rather than given”.

2. The example does not give any algorithm for constructing a string of characters that is a computer program.

3. The program(s) are found in a set of rules.

4. However, whatever and whoever creates those rules, since there is no algorithm given for constructing a string of characters that is a computer programs (2), that string of characters that is the computer program was constructed by a person. (In fact it was and must be.)

5. This is not program Synthesis. (1,4)

6. Furthermore, there is no proof that “x<y ? y : x” is appropriate for the given specification (as required in your definition of program synthesis) because no formal definition of the ? : operator is given or used to relate it to the given specification.

The above applies to every program you can create using such a set of rules. You are simply hard-coding a set of programs and their associated specifications in preparation for their being requested and will fail if any other programs are required. This is tantamount to a Programming Library of common functions being coded and made available to the programmer. Program Synthesis allows any program specification that can be expressed to be entered.

Which lines do you not agree with and why? And please, no appealing to authority rather than logic and reasoning. Galileo said, “In questions of science, the authority of a thousand is not worth the humble reasoning of a single individual.”

No offense, ok?

M. Davis — Preceding unsigned comment added by Mdaviscs (talk • contribs) 06:40, 8 March 2020 (UTC)

“As for loop constructs, please note that the approach is able to generate recursive programs (w.r.t. arbitrary well-founded induction orderings), as demonstrated in the quotient remainder example in Manna.Waldinger.1980. This makes it Turing-complete. Make sure you understand what a functional programming language is, and what Turing complete means.”

Yes, Turing Complete means (implies) programs must have loops and functional programming implements loops via recursive programs. That requires a program declaration and invocation that your single expressions do not include.

“The section in question presents one approach to program synthesis along published journal articles. I can't help if you don't like the approach. I'm tired of defending it.”

Manna & Waldinger 1980 does not utilize rules which include a computer program written by a person as you do in column Program. Where does that occur? Here is an on-line copy: https://my.pcloud.com/publink/show?code=XZtBynkZ8plGfSrSLEhACWt4pWA9D0Q8YtXX All of their table entries consist of standard mathematical expressions deduced from the specification. You manually add a computer program and the whole point of the process is to create that computer program automatically. Mdaviscs (talk) 18:42, 9 March 2020 (UTC)

Reply:

• Ad 1.: What you describe is automated program synthesis. The lead clearly mentions "different degrees of automation". The Manna / Waldinger approach is not automated.
• Ad 2.: That's right. The approach provides a formal framework for manual reasoning instead.
• Ad 3.: Programs are constructed by applying a set of rules. Some rules contain (in the "Program" column) program parts (like "?:" in line 58; when a recursive program is to be synthesized, an induction proof has to be performed, and that column contains a recursive call, corresponding to an induction hypothesis). During the reasoning process, these program parts are assembled to form larger parts, and eventually the program; this is achieved by the resolution rules.
• Ad 4.: A minimal rules set has been created by Manna / Waldinger, and proven sound (i.e. applying them can generate only programs that satisfy the original specification). In many case studies (I added a list of examples, with references), more background knowledge was added in form of axioms (similar to line 1,2,3 in the trivial example under debate).
• Ad 5.: I hope that you'll agree that - after considering my corrections for 1-4 - the approach can be subsumed under (non-automatic) program synthesis. It is definitely different from "chosing a program for a list".
• Ad 6.: The definition of "?:" should be found in the cited 1980 paper, along with the soundness proof of the reasoning rules. The latter implies the appropriateness of “x<y ? y : x”, since it was obtained by strictly following the approach's reasoning rules.

The external link you gave points to the same paper I used to write the article section. I believe I summarized it correctly. I suggest you read it, and restrict your complaints to deviances between paper and wikipedia article. E.g. line 58, which introduces the often-debated "?:", is explained on 100. Recursive programs are synthesized beginning on p.103. - Jochen Burghardt (talk) 20:18, 9 March 2020 (UTC)

Page isn't protected anymore, so the request is moot. –MJL ‐Talk‐^☖ 17:25, 11 March 2020 (UTC)

You state "the system is far from being automatic" however "Program synthesis is the task of automatically finding a program in the underlying programming language that satisfies the user intent expressed in the form of some specification." ~ Sumit Gulwani, Oleksandr Polozov and Rishabh Singh (2017), "Program Synthesis", Foundations and Trends® in Programming Languages: Vol. 4: No. 1-2, pp 1-119. https://www.nowpublishers.com/article/Details/PGL-010.

This is just 1 of 7 references that I gave to this fact. No references to it being a manual procedure have been given.

"As a toy example . . . [citation needed]" is an inappropriate reference since it is not automatic, and needs to be removed. It is not cited and there are numerous contrary citations.

"Program synthesis is the task of automatically finding a program in the underlying programming language that satisfies the user intent expressed in the form of some specification. Since the inception of AI in the 1950s, this problem has been considered the holy grail of Computer Science."

This is clearly saying that Program Synthesis has always been the process of automating computer programming. How could it possibly be a "holy grail" to come up with a way to choose a program from a list of programs provided? I am not faulting what Manna/Waldinger did. I am saying it is not true to call it an "example of Program Synthesis". Don't call it that. Call it "an attempt to make progress toward that goal" if you wish. If they had an automated way, they would show it instead of a manual way. They don't. Mdaviscs (talk) 15:13, 19 August 2021 (UTC)