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.
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.
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.
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.
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.
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".
[+] [-] kasbah|9 years ago|reply
> 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=PLXr4KViVC0...
[2]: http://research.microsoft.com/en-us/um/people/sumitg/flashfi...
[+] [-] vanderZwan|9 years ago|reply
Sumit Gulwani - Data Manipulation using Programming By Examples and Natural Language
https://www.youtube.com/watch?v=uqV9BlxEG5s
[+] [-] unimpressive|9 years ago|reply
[+] [-] tikhonj|9 years ago|reply
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|9 years ago|reply
[+] [-] kasbah|9 years ago|reply
[+] [-] LaPrometheus|9 years ago|reply
https://courses.cs.washington.edu/courses/cse507/16sp/
[+] [-] echelon|9 years ago|reply
[+] [-] theoh|9 years ago|reply
[+] [-] bbcbasic|9 years ago|reply
Would it be useful for creating a DSL for example?
[+] [-] lmeyerov|9 years ago|reply
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|9 years ago|reply
http://research.microsoft.com/en-us/um/people/sumitg/flashfi...
[+] [-] LaPrometheus|9 years ago|reply
http://emina.github.io/rosette/apps.html
[+] [-] spynxic|9 years ago|reply
Just curious, are the products of all programs formula? Worded differently, are the products of all functions formula?
[+] [-] tikhonj|9 years ago|reply
[+] [-] profquail|9 years ago|reply
https://en.wikipedia.org/wiki/Curry–Howard_correspondence
[+] [-] PaulHoule|9 years ago|reply
[+] [-] cpchen|9 years ago|reply
[+] [-] dylz|9 years ago|reply