HN Theater @HNTheaterMonth

This is an active field of research. Search for "program synthesis".

We are advancing, but the current state is... not mind-blowing yet (albeit somewhat cool!). See [1] for an example interactive demo and [2] for the corresponding presentation.

[1] http://comcom.csail.mit.edu/comcom/#Synquid

[2] https://www.youtube.com/watch?v=HnOix9TFy1A

⬐ hwayne

I was in the audience for that talk. The recording doesn't capture how much energy there was- we were all gasping and cheering throughout.

Still a decade off from production, though. That it doesn't just take "test cases": you have to know how to formally express the program properties, which is a separate skill from both unit testing and implementing.

https://www.youtube.com/watch?v=hhGnMbw98u8

https://www.youtube.com/watch?v=tfnldxWlOhM

https://www.youtube.com/watch?v=HnOix9TFy1A

https://pron.github.io/posts/tlaplus-curryon-talk

https://learntla.com/introduction/

https://leanprover.github.io/theorem_proving_in_lean/

https://rise4fun.com/dafny

For an introduction and motivation to TLA+ I recommend Hillel Wayne's talk Everything About Distributed Systems is Terrible [0] and basically anything he has written on his blog about the TLA+.

I think following along with the TLA+ video course is really thorough and digestible once you've decided that you want to learn more [1].

You'll find the TLA+ Hyperbook is a useful reference and guide as you start specifying your own systems [2]. It has a number of examples and projects to work on.

Eventually if you want to go deep after you've decided it's worth it for yourself, get into Specifying Systems the text book and bible of TLA+ [3].

Program Synthesis has a lot of research in it and is starting to show promising results. I'd say that while the research has been going on for a long time it's still rather new to industrial use... for a motivating talk and explanation on what program synthesis is try this one: https://www.youtube.com/watch?v=HnOix9TFy1A

[0] https://www.hillelwayne.com/talks/distributed-systems-tlaplu...

[1] https://lamport.azurewebsites.net/video/videos.html

[2] https://lamport.azurewebsites.net/tla/hyperbook.html

[3] https://lamport.azurewebsites.net/tla/book.html

⬐ deegles

Thanks!

> Good specifications are often written at a level that generating executable code from them is often undecidable and almost always intractable in practice.

What about modern dependently-typed meta languages like Idris and program synthesizers like Nadia Polikarpova's work on Synquid?

Type-Driven Program Synthesis, by Nadia Polikarpova (StrangeLoop 2018) [video] https://www.youtube.com/watch?v=HnOix9TFy1A

MIT Comcom: Synquid program synthesizer, and more command-line tools for the web

http://comcom.csail.mit.edu/comcom/

Idris Software Foundations https://github.com/idris-hackers/software-foundations

⬐ pron

We don't know how to scale those [1]. It's very easy to specify a simple sorting function in Idris/Java with JML and prove it correct. It's a whole other matter to specify the global properties of an entire system, and verify them all the way down to the small bits of code. Various code synthesis tools are even more limited, as they tend to rely heavily on fragile automated reasoning tools like SMT solvers, although both are orders of magnitude away from being able to handle real applications that I think that comparing them to one another is a bit beside the point.

The biggest programs ever written and verified with deductive proofs -- be it dependently typed languages or any verification based on deduction, correspond at most to ~10,000 LOC of C, taken years of work by academic experts, and had to be significantly simplified to make proofs easier (i.e., they had to use only the simplest data structures, etc.). In contrast, business applications are 2-3 orders of magnitude bigger.

[1]: And when I say "we don't know" I mean that it is possible that some time in the next 2-5 decades we may be able to do something, but it's also possible that there are fundamental complexity limitations that mean that this particular path will never lead to something similar to what we may imagine it could.

⬐ danidiaz

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

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

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

[2] Strange Loop 2018 talks (80 videos) 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

* All the Languages Together, by Amal Ahmed 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

* Data Driven UIs, Incrementally, by Yaron Minsky 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

* A Little Taste of Dependent Types, by David Christiansen https://www.youtube.com/watch?v=VxINoKFm-S4

* You are a Program Synthesizer, by James Koppel 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

⬐ flashgordon

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

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?

⬐ ilovecaching

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.