© 2020 Strange Loop
Over the best decade, program synthesis has gone from twiddling bits to making web browsers. And the insights behind these systems can also be used by a much older and better program synthesizer: you.
In this talk, I'll explain how program synthesis and verification works from the angle of what they can teach us about normal programming. I'll explain how notions of code quality are really based on mathematical and mental constructs which are ethereal in programming, but concrete in theorem proving. You'll learn the process of deriving code from a specification, and why some parts of the code synthesize instantly, while others take cleverness. I'll show you how to use Hoare logic to analyze your code's complexity, how to use abstract interpretation to count the "states" of code, and how it's possible for straight-line code to contain a conditional. At the end of this talk, you'll have a better idea of what makes good vs. bad code, and how bad code makes life difficult for all kinds of program synthesizers, both machine and human.
Jimmy is a serial entrepreneur and current Ph. D. candidate in the Computer-Aided Programming Group at MIT. By day, he works at MIT trying to make program transformation and synthesis tools easier to build ("programs that write programs that write programs"), and by night he teaches software engineers how to write better code. Before MIT, he was the third employee of Apptimize, and the founder of Tarski Technologies, a startup pursuing automated bug-fixing. He was named a "20 Under 20" Thiel Fellow in 2012, and is a native of St. Louis.