there's decades and decades of work making formal verification easy and integrated
Conversation
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
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.
We kind of need some kind of ‘productionise formal methods trading scheme’ or something 😂