CS294: Program Synthesis for Everyone • Hacker News Board

Re: CS294: Program Synthesis for Everyone

#21

Post by kasbah » Mon, Nov 21, 2016, 12:53 PM UTC

vanderZwan wrote: post #17

kasbah wrote: post #11

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…

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

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.

Re: CS294: Program Synthesis for Everyone

#22

Post by spynxic » Mon, Nov 21, 2016, 11:48 PM UTC

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?

Re: CS294: Program Synthesis for Everyone

#23

Post by profquail » Tue, Nov 22, 2016, 12:07 PM UTC

spynxic wrote: post #22

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?

Yes - that's the Curry-Howard isomorphism:

https://en.wikipedia.org/wiki/Curry–Howard_correspondence

Re: CS294: Program Synthesis for Everyone

#24

Post by tikhonj » Tue, Nov 22, 2016, 10:48 PM UTC

spynxic wrote: post #22

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?

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".