4 ms·

Type-Driven Program Synthesis [video]

59 points by espeed 8y ago

ilovecaching 8y ago
UCSD does a lot of cool type system stuff. Also check out Liquid Haskell (another UCSD project), a refinement type system added to Haskell. A good book to read to learn more about the crazy things you can do with a dependent type system is the Idris O'reilly book as well. If you're like me and think modern software practices are scarily inadequate at proving correctness, but you still need high performance, take a look at Rust. It also has a very nice type system with ADTs, and it's being improved all the time. Unlike Haskell and Idris, it's not geared towards research and has no GC, so it has near C/C++ performance.
danidiaz 8y ago
Another good talk about using types to guide your programming—instead of merely checking it for errors—is "Is a type a lifebuoy or a lamp?" by Conor McBride https://skillsmatter.com/skillscasts/8893-is-a-type-a-lifebuoy-or-a-lamp https://skillsmatter.com/skillscasts/8893-is-a-type-a-lifebu... It is best approached with some knowledge about how the Haskell typeclass mechanism works. The second part of the talk (from 25:50) is about how to expand the traditional Haskell Hindley-Milner type system (which is very centered on avoiding the need for explicit type annotations, using type inference) to allow the user to provide more explicit type information, which pays off by automating the generation of parts of the term-level code.
- AlexCoventry 8y ago
  Is there an alternative source for this? I'd like to watch it at higher speed, and vimeo doesn't seem to be providing a way to speed it up, or to download it independent of my skills matter login.
espeed 8y ago
Type-driven development, meta languages, specs, provably correct code, and automatic code generation were some of the big overlapping themes at Strange Loop [1] this year. All the talks posted online this week [2], and I've posted links to some of the related videos below [3]. It's a good indicator that the time has come for an idea when multiple lines of research and projects from disparate domains begin converging on the same idea from different directions. Several facets of the puzzle I've been working the last few years have converged towards this area so it's good to see that it's not just me, maybe that means we're all on the right track. But as 'pron and those who have been working in this area have pointed out [4], this part of the puzzle is not yet solved, and one of the primary open issues is how to scale it to the system level (beyond provably correct programs to provably correct systems). One of the questions I've been pondering is how can we combine provably correct software specs with hardware specs identified for any given system to find the optimal data structures and algorithms given the constraints of that architecture. Does something similar already exist? What's the best software currently out there for simulating ideal data flow for a given hardware configuration and a given set of system constraints? [1] Strange Loop https://www.thestrangeloop.com https://www.thestrangeloop.com [2] Strange Loop 2018 talks (80 videos) https://www.youtube.com/playlist?list=PLcGKfGEEONaBUdko326yL6ags8C_SYgqH https://www.youtube.com/playlist?list=PLcGKfGEEONaBUdko326yL... [3] Related videos... * Vellvm - Verifying the LLVM, by Steve Zdancewic https://www.youtube.com/watch?v=q6gSC3OxB_8 https://www.youtube.com/watch?v=q6gSC3OxB_8 * All the Languages Together, by Amal Ahmed https://www.youtube.com/watch?v=3yVc5t-g-VU https://www.youtube.com/watch?v=3yVc5t-g-VU * Towards Language Support for Distributed Systems, by Heather Miller https://www.youtube.com/watch?v=IeBbiQZYmuY https://www.youtube.com/watch?v=IeBbiQZYmuY * Data Driven UIs, Incrementally, by Yaron Minsky https://www.youtube.com/watch?v=R3xX37RGJKE https://www.youtube.com/watch?v=R3xX37RGJKE * Proof Theory Impressionism: Blurring the Curry-Howard Line, by Dan Pittman https://www.youtube.com/watch?v=jrVPB-Ad5Gc https://www.youtube.com/watch?v=jrVPB-Ad5Gc * A Little Taste of Dependent Types, by David Christiansen https://www.youtube.com/watch?v=VxINoKFm-S4 https://www.youtube.com/watch?v=VxINoKFm-S4 * You are a Program Synthesizer, by James Koppel https://www.youtube.com/watch?v=ldkF-4WNZqA https://www.youtube.com/watch?v=ldkF-4WNZqA [4] open issue is how to scale it to the system level https://news.ycombinator.com/item?id=18253680 https://news.ycombinator.com/item?id=18253680
flashgordon 8y ago
Wow this was such an awesome viewing. I have found amazing work from the refinement typing folks at USCD. The book by Ranjit Dhalla is a gold mine! http://goto.ucsd.edu/~rjhala/lh-book-draft.pdf http://goto.ucsd.edu/~rjhala/lh-book-draft.pdf One question I had was can this be extended to type-drive "type" synthesis to derive new types and then use that to synthesize programs?

59 points by espeed 8y ago

UCSD does a lot of cool type system stuff. Also check out Liquid Haskell (another UCSD project), a refinement type system added to Haskell. A good book to read to learn more about the crazy things you can do with a dependent type system is the Idris O'reilly book as well. If you're like me and think modern software practices are scarily inadequate at proving correctness, but you still need high performance, take a look at Rust. It also has a very nice type system with ADTs, and it's being improved all the time. Unlike Haskell and Idris, it's not geared towards research and has no GC, so it has near C/C++ performance.

danidiaz 8y ago

Another good talk about using types to guide your programming—instead of merely checking it for errors—is "Is a type a lifebuoy or a lamp?" by Conor McBride https://skillsmatter.com/skillscasts/8893-is-a-type-a-lifebuoy-or-a-lamp https://skillsmatter.com/skillscasts/8893-is-a-type-a-lifebu... It is best approached with some knowledge about how the Haskell typeclass mechanism works. The second part of the talk (from 25:50) is about how to expand the traditional Haskell Hindley-Milner type system (which is very centered on avoiding the need for explicit type annotations, using type inference) to allow the user to provide more explicit type information, which pays off by automating the generation of parts of the term-level code.

AlexCoventry 8y ago
Is there an alternative source for this? I'd like to watch it at higher speed, and vimeo doesn't seem to be providing a way to speed it up, or to download it independent of my skills matter login.

espeed 8y ago

Type-driven development, meta languages, specs, provably correct code, and automatic code generation were some of the big overlapping themes at Strange Loop [1] this year. All the talks posted online this week [2], and I've posted links to some of the related videos below [3]. It's a good indicator that the time has come for an idea when multiple lines of research and projects from disparate domains begin converging on the same idea from different directions. Several facets of the puzzle I've been working the last few years have converged towards this area so it's good to see that it's not just me, maybe that means we're all on the right track. But as 'pron and those who have been working in this area have pointed out [4], this part of the puzzle is not yet solved, and one of the primary open issues is how to scale it to the system level (beyond provably correct programs to provably correct systems). One of the questions I've been pondering is how can we combine provably correct software specs with hardware specs identified for any given system to find the optimal data structures and algorithms given the constraints of that architecture. Does something similar already exist? What's the best software currently out there for simulating ideal data flow for a given hardware configuration and a given set of system constraints? [1] Strange Loop https://www.thestrangeloop.com https://www.thestrangeloop.com [2] Strange Loop 2018 talks (80 videos) https://www.youtube.com/playlist?list=PLcGKfGEEONaBUdko326yL6ags8C_SYgqH https://www.youtube.com/playlist?list=PLcGKfGEEONaBUdko326yL... [3] Related videos... * Vellvm - Verifying the LLVM, by Steve Zdancewic https://www.youtube.com/watch?v=q6gSC3OxB_8 https://www.youtube.com/watch?v=q6gSC3OxB_8 * All the Languages Together, by Amal Ahmed https://www.youtube.com/watch?v=3yVc5t-g-VU https://www.youtube.com/watch?v=3yVc5t-g-VU * Towards Language Support for Distributed Systems, by Heather Miller https://www.youtube.com/watch?v=IeBbiQZYmuY https://www.youtube.com/watch?v=IeBbiQZYmuY * Data Driven UIs, Incrementally, by Yaron Minsky https://www.youtube.com/watch?v=R3xX37RGJKE https://www.youtube.com/watch?v=R3xX37RGJKE * Proof Theory Impressionism: Blurring the Curry-Howard Line, by Dan Pittman https://www.youtube.com/watch?v=jrVPB-Ad5Gc https://www.youtube.com/watch?v=jrVPB-Ad5Gc * A Little Taste of Dependent Types, by David Christiansen https://www.youtube.com/watch?v=VxINoKFm-S4 https://www.youtube.com/watch?v=VxINoKFm-S4 * You are a Program Synthesizer, by James Koppel https://www.youtube.com/watch?v=ldkF-4WNZqA https://www.youtube.com/watch?v=ldkF-4WNZqA [4] open issue is how to scale it to the system level https://news.ycombinator.com/item?id=18253680 https://news.ycombinator.com/item?id=18253680

flashgordon 8y ago

Wow this was such an awesome viewing. I have found amazing work from the refinement typing folks at USCD. The book by Ranjit Dhalla is a gold mine! http://goto.ucsd.edu/~rjhala/lh-book-draft.pdf http://goto.ucsd.edu/~rjhala/lh-book-draft.pdf One question I had was can this be extended to type-drive "type" synthesis to derive new types and then use that to synthesize programs?