with potential enormous wins in terms of testing that doesn't need to be done, vulnerabilities not fixed, etc.
Conversation
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
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
My current problem at is ‘parse optentype safely’. This has a bunch of side benefits like learning about dependent type systems, both from a users perspective, and an implementors perspective, and digging up some old research on ways of describing binary formats.
1
At the moment it’s out of the goodness of our hearts, but I wish it weren’t so. Other companies I’ve been at are super reckless about this stuff.
1
1
We kind of need some kind of ‘productionise formal methods trading scheme’ or something 😂