An Intro to Program Synthesis

00:00 Introduction
2:19 Part 1: Overview of Hoare Logic
4:05 Part 1 - Assertions are not states
8:29 Part 1 - If and Sequence rules
10:21 Part 1 - Weakest Preconditions
12:53 Part 1 - Automatic Verification
14:08 Part 2: Loops and Verification Conditions
17:43 Part 2 - The Verification Condition Tradeoff
20:19 Part 2 - While rule and loop invariants
22:00 Part 2 - Verification Condition for loops
26:35 Part 3: Using a program synthesizer (Sketch)
31:04 Part 3 - Implementing formulas in Sketch
33:04 Part 3 - Defining inv()
34:58 Part 4: CounterExample-Guided Inductive Synthesis (CEGIS)
35:36 Part 4 - Deduction vs Induction
38:00 Part 4 - Deductive Synthesis
40:16 Part 4 - Inductive Synthesis
41:18 Part 4 - The Sketching programming paradigm
42:46 Part 4 - Control Functions
43:55 Part 4 - Simple Denotational Semantics
47:36 Part 4 - Semantics of Holes
49:06 Part 4 - Denotation for Commands
50:44 Part 4 - Semantics of assert
51:44 Part 4 - Sketch Resolution
52:57 Part 4 - Bounded Observation Hypothesis
55:08 Part 4 - CEGIS algorithm
59:13 Part 4 - Practical considerations

Slides: https://docs.google.com/presentation/...

Notes (these may confuse you more if you read them before understanding the main content):
Armando's thesis: https://citeseerx.ist.psu.edu/documen...
10:04: These rules also describe the weakest precondition of the commands. But, IMO, the following presentation of loop-free weakest preconditions makes more sense:
• wpc(x := e, B) = B[x → e]
• wpc(c1;c2, B) = wpc(c1, wpc(c2, B))
• wpc(if b then c1 else c2, B) = (b ∧ wpc(c1, B)) ∨ (¬b ∧ wpc(c2, B))

25:10: It matters that the antecedent is (I /\ -cond) and not just -cond (which would be what one would infer from the text). The I gives "more power" to prove that we get B. In other words, -cond alone may not be enough. This is a similar reason of why in the 'while' rule, the precondition in the assumption is {{I /\ cond}} and not just {{I}} (even though the latter would also be correct; it's just the former allows us to prove more programs)
33:50: In practice, it's pretty hard to even compile Sketch and get it to run. But also, while this example ran some months ago and I could get this invariant, I tried running it again a couple of days ago and it didn't terminate.
34:34: I use this as a basis: https://softwarefoundations.cis.upenn...
36:18: You can find a good intro to scientific inference in "Philosophy of Science, A Very Short Introduction", by Samir Okasha, Chapter 2. Ladyman, in Section 1.3 of "Understanding Philosophy of Science" also provides an introduction, which is less crisp but more extensive.
38:24: If you want to learn more about constructive logic and extraction of programs, you can look up "Proofs as Programs" or "Curry-Howard Correspondence". Unfortunately, I don't have good introductory material to suggest.
39:15: The example is taken from: Manna, Zohar, and Richard J. Waldinger. "Toward automatic program synthesis." Communications of the ACM 14.3 (1971): 151-165. Fun fact: The editor of the proceedings where this paper appeared is Gries, the author of "A Science of Programming"
48:23: We could also define it: A[??]σφ = φ(??)
59:44: The x and y axis labels are flipped.

Compiler Meetup at UIUC: https://compiler-meetup.cs.illinois.edu/