4 ms·

CS294: Program Synthesis for Everyone

241 points by nickmain 10y ago

PaulHoule 10y ago
Nice to see this done at the 2 level.
- cpchen 10y ago
  In UC Berkeley, the 2 level means graduate student level.
- dylz 10y ago
  <100s were freshman/sophomore undergrad. 2 level isn't what you think, I assume
tikhonj 10y ago
Oh hey, I actually took this class. Funny to see it linked on HN. It was easily the single most valuable class I took in undergrad. There's definitely a lot of useful information there, but I'm not sure how well it's organized because the course website wasn't designed to stand on its own.
- quantumtremor 10y ago
  Unfortunately Ras Bodik is no longer at Berkeley, so it's unlikely it'll be offered again.
- kasbah 10y ago
  I am planning to go through this course virtually from the material linked. Would you mind if I get in touch with you if I get stuck on something?
  - tikhonj 10y ago
    Sure, although I'm not sure how much I remember of any given topic :P.
LaPrometheus 10y ago
An advanced version of this course, by one of the teachers of CS294. https://courses.cs.washington.edu/courses/cse507/16sp/ https://courses.cs.washington.edu/courses/cse507/16sp/
echelon 10y ago
I'm not familiar with this discipline. What might this subject matter be used for? Is this related to ML in a broader sense?
- theoh 10y ago
  It's about making tools that help with the structural aspects of generating code. It's not part of machine learning, but rather it's very much about symbolic/analytic/logical production of code based on a specification of some sort.
  - SolarNet 10y ago
    I mean just about every thing was AI at one point; program synthesis was seen as AI (like in the 70s) right up until it wasn't after we effectively encoded it into programming languages. For example lisp it self was effectively AI research as well. In computer science it's pretty typical to refer to things as AI right up until we understand how to engineer it; the history of email that was posted recently is a great example (at first we just had computers extracting features and learning things, and it was vague and generic; these days we understand the system as a reputation network, and we understand the details of each of the features because it required a bunch of engineering to make that specific solution scale and fast).
bbcbasic 10y ago
Can someone give me the layman summary of this. I.e. what day to day problem could this be useful to solve? Would it be useful for creating a DSL for example?
- LaPrometheus 10y ago
  A list of applications built on top of Rosette: http://emina.github.io/rosette/apps.html http://emina.github.io/rosette/apps.html
- kasbah 10y ago
  I think the clearest example of an application that comes from these techniques is Excel Flash Fill and this course goes over the algorithm used in the Flash Fill paper. http://research.microsoft.com/en-us/um/people/sumitg/flashfill.html http://research.microsoft.com/en-us/um/people/sumitg/flashfi...
- lmeyerov 10y ago
  The same concept is behind Viv, the successor to Siri: http://www.esquire.com/lifestyle/a34630/viv-artificial-intelligence-0515/ http://www.esquire.com/lifestyle/a34630/viv-artificial-intel... A lot of the recent work here takes advantage of SMT solvers (next generation of SAT solvers), but that's not necessary. As with Viv and Flash Fill, a lot of it is about changing the concept of what it means to write a program, and use alternative approaches to "complete" it. As another example, generating 0-day bug fixes based on how code "should" look, or recommending typed completions to gaps in code. For my past work in that group, I looked at "sketching" efficient schedules for parallel code, where I only specified the bits I cared about. Nowadays, I think about automatically generating queries for visual analytics.
kasbah 10y ago
Nice to see this do so well over here. I posted this to /r/Racket earlier and as I said over there: > This has screencasts or at least slides for most lectures. I have just started going through it myself and plan to "audit" all the lectures and do the homework assignments. Anyone have an interest in this and would like a virtual study buddy? It's also worth pointing out that this excellent RacketCon talk [1] made me go seek out more about Excel Flash Fill [2] and in seeking to understand how that works I stumbled upon this course. [1]: https://www.youtube.com/watch?v=nOyIKCszNeI&list=PLXr4KViVC0qKSiKGO6Vz9EtxUfKPb1Ma0 https://www.youtube.com/watch?v=nOyIKCszNeI&list=PLXr4KViVC0... [2]: http://research.microsoft.com/en-us/um/people/sumitg/flashfill.html http://research.microsoft.com/en-us/um/people/sumitg/flashfi...
- unimpressive 10y ago
  You don't have contact info on your profile, re: study buddy.
  - kasbah 10y ago
    Ah, thanks, you can email me: kaspar.emanuel@gmail.com.
- vanderZwan 10y ago
  BTW, here's a detailed technical talk about that Excel Flash Fill thing from last year's Curry On! conference: Sumit Gulwani - Data Manipulation using Programming By Examples and Natural Language https://www.youtube.com/watch?v=uqV9BlxEG5s https://www.youtube.com/watch?v=uqV9BlxEG5s
  - kasbah 10y ago
    Thanks for linking that! I hadn't seen it and I _had_ been searching YouTube for lectures on FlashFill but the popularity of this feature made it hard to find anything other than tutorials on using it in Excel.
spynxic 10y ago
There is a section named, "Compile your programs to formulas" Just curious, are the products of all programs formula? Worded differently, are the products of all functions formula?
- profquail 10y ago
  Yes - that's the Curry-Howard isomorphism: https://en.wikipedia.org/wiki/Curry–Howard_correspondence https://en.wikipedia.org/wiki/Curry–Howard_correspondence
- tikhonj 10y ago
  I'm not sure what you mean by this question. What that lecture covers is essentially how to express an approximation of the operational semantics of a simple language as a logic formula in a very specific kind of logic (ie one of the theories supported by the Z3 SMT solver). It only supports a small number of constructs and data types, and handles infinite loops by placing an arbitrary bound on how far a program can run. It doesn't tell you anything about "all programs" or "all functions".

241 points by nickmain 10y ago

PaulHoule 10y ago

Nice to see this done at the 2 level.

cpchen 10y ago
In UC Berkeley, the 2 level means graduate student level.
dylz 10y ago
<100s were freshman/sophomore undergrad. 2 level isn't what you think, I assume

tikhonj 10y ago

Oh hey, I actually took this class. Funny to see it linked on HN. It was easily the single most valuable class I took in undergrad. There's definitely a lot of useful information there, but I'm not sure how well it's organized because the course website wasn't designed to stand on its own.

quantumtremor 10y ago
Unfortunately Ras Bodik is no longer at Berkeley, so it's unlikely it'll be offered again.
kasbah 10y ago
I am planning to go through this course virtually from the material linked. Would you mind if I get in touch with you if I get stuck on something?
- tikhonj 10y ago
  Sure, although I'm not sure how much I remember of any given topic :P.

LaPrometheus 10y ago

An advanced version of this course, by one of the teachers of CS294. https://courses.cs.washington.edu/courses/cse507/16sp/ https://courses.cs.washington.edu/courses/cse507/16sp/

echelon 10y ago

I'm not familiar with this discipline. What might this subject matter be used for? Is this related to ML in a broader sense?

theoh 10y ago
It's about making tools that help with the structural aspects of generating code. It's not part of machine learning, but rather it's very much about symbolic/analytic/logical production of code based on a specification of some sort.
- SolarNet 10y ago
  I mean just about every thing was AI at one point; program synthesis was seen as AI (like in the 70s) right up until it wasn't after we effectively encoded it into programming languages. For example lisp it self was effectively AI research as well. In computer science it's pretty typical to refer to things as AI right up until we understand how to engineer it; the history of email that was posted recently is a great example (at first we just had computers extracting features and learning things, and it was vague and generic; these days we understand the system as a reputation network, and we understand the details of each of the features because it required a bunch of engineering to make that specific solution scale and fast).

bbcbasic 10y ago

Can someone give me the layman summary of this. I.e. what day to day problem could this be useful to solve? Would it be useful for creating a DSL for example?

LaPrometheus 10y ago
A list of applications built on top of Rosette: http://emina.github.io/rosette/apps.html http://emina.github.io/rosette/apps.html
kasbah 10y ago
I think the clearest example of an application that comes from these techniques is Excel Flash Fill and this course goes over the algorithm used in the Flash Fill paper. http://research.microsoft.com/en-us/um/people/sumitg/flashfill.html http://research.microsoft.com/en-us/um/people/sumitg/flashfi...
lmeyerov 10y ago
The same concept is behind Viv, the successor to Siri: http://www.esquire.com/lifestyle/a34630/viv-artificial-intelligence-0515/ http://www.esquire.com/lifestyle/a34630/viv-artificial-intel... A lot of the recent work here takes advantage of SMT solvers (next generation of SAT solvers), but that's not necessary. As with Viv and Flash Fill, a lot of it is about changing the concept of what it means to write a program, and use alternative approaches to "complete" it. As another example, generating 0-day bug fixes based on how code "should" look, or recommending typed completions to gaps in code. For my past work in that group, I looked at "sketching" efficient schedules for parallel code, where I only specified the bits I cared about. Nowadays, I think about automatically generating queries for visual analytics.

kasbah 10y ago

Nice to see this do so well over here. I posted this to /r/Racket earlier and as I said over there: > This has screencasts or at least slides for most lectures. I have just started going through it myself and plan to "audit" all the lectures and do the homework assignments. Anyone have an interest in this and would like a virtual study buddy? It's also worth pointing out that this excellent RacketCon talk [1] made me go seek out more about Excel Flash Fill [2] and in seeking to understand how that works I stumbled upon this course. [1]: https://www.youtube.com/watch?v=nOyIKCszNeI&list=PLXr4KViVC0qKSiKGO6Vz9EtxUfKPb1Ma0 https://www.youtube.com/watch?v=nOyIKCszNeI&list=PLXr4KViVC0... [2]: http://research.microsoft.com/en-us/um/people/sumitg/flashfill.html http://research.microsoft.com/en-us/um/people/sumitg/flashfi...

unimpressive 10y ago
You don't have contact info on your profile, re: study buddy.
- kasbah 10y ago
  Ah, thanks, you can email me: kaspar.emanuel@gmail.com.
vanderZwan 10y ago
BTW, here's a detailed technical talk about that Excel Flash Fill thing from last year's Curry On! conference: Sumit Gulwani - Data Manipulation using Programming By Examples and Natural Language https://www.youtube.com/watch?v=uqV9BlxEG5s https://www.youtube.com/watch?v=uqV9BlxEG5s
- kasbah 10y ago
  Thanks for linking that! I hadn't seen it and I _had_ been searching YouTube for lectures on FlashFill but the popularity of this feature made it hard to find anything other than tutorials on using it in Excel.

spynxic 10y ago

There is a section named, "Compile your programs to formulas" Just curious, are the products of all programs formula? Worded differently, are the products of all functions formula?

profquail 10y ago
Yes - that's the Curry-Howard isomorphism: https://en.wikipedia.org/wiki/Curry–Howard_correspondence https://en.wikipedia.org/wiki/Curry–Howard_correspondence
tikhonj 10y ago
I'm not sure what you mean by this question. What that lecture covers is essentially how to express an approximation of the operational semantics of a simple language as a logic formula in a very specific kind of logic (ie one of the theories supported by the Z3 SMT solver). It only supports a small number of constructs and data types, and handles infinite loops by placing an arbitrary bound on how far a program can run. It doesn't tell you anything about "all programs" or "all functions".