"Production" programming languages have been cribbing off ancient academic research for years now (functional), but I have a feeling that well is running dry and I'm not sure there are any obvious wins coming down the pipe
Conversation
there's decades and decades of work making formal verification easy and integrated
1
10
with potential enormous wins in terms of testing that doesn't need to be done, vulnerabilities not fixed, etc.
1
8
For certain critical domains it's long overdue. But general purpose? I'm not so sure.
1
strong properties in certain domains, weak properties everywhere
1
2
I honestly don't know what this would look like. Refinement types? How do you avoid shoving the whole complexity of the type system on all the users?
2
1
Rust shows notions like linearity/ownership/borrowing could go mainstream; there’s a lot of use cases for refinement types that are simpler (IMO).
1
4
Yeah, I wish we had some way to fund teams to work on the intermediate step of turning stuff from academia into nicely designed/built production grade tools, based on the on-the-ground learnings from industry.
2
6
Atm I find the formal methods tools impressive, but super clunky from a dev perspective. Need more work on pulling in learnings from industry to polish this stuff up nicely.
I really think that dependent types and refinment types could go mainstream if we invested time in cleaning up the develper experience, languages, and toolchains. But your right that this is not a job that we should burden universities with.
1