"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.
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.
1
2
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
This is where I was going with the "problem statement" thing. If you want to spin up a team with 10 senior engineers to produce nothing for three years, you need something to sell mgmt. The CLR was, "stop devs writing memory corruption bugs that threaten MSFT survival."
2
3
Java was "make it easier for people to run code on Sun with no modifications." I presume Rust was something like, "we can't reasonably write parallel code in Firefox." I don't know what the next problem is.
2
Show replies