HN Theater @HNTheaterMonth

⬐ VictorSCushman

We're looking at formal verification methods as part of my senior design project. For the longest time I thought formal verification was more of an afterthought, but as the project has grown, and as I've seen talks and literature showing the benefits of formal verification, I'm now in the camp that all (or at least all serious production...) languages/implementations should prioritize verification.

⬐ jewelry_wolf

When I took one of my first computer science classes, the teacher said never challenge compiler as it's always right. Check your own code. After years of practice in the industry, I'm not that naive boy anymore and I'm pretty sure every system has bug. The only difference is how many times the golden path has been verified, and how wide is that path.

⬐ lou1306

"Always right" is indeed hyperbolic, however the "never challenge compilers" is still good advice. I guess it would be very, very difficult for a human to apply the same optimization passes while introducing less bugs than a compiler would.

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