My point is that the "what's possible" part covers principally activities that most users don't want to do: express and prove complex system invariants. It's not at all clear what those are for most programs, and the effort to define them gets you nowhere closer to "shipping".
Conversation
It would, IOW, take a major shift to the economic priorities of people working in software. Maybe that might happen (I'd love it if it did) but I'm not seeing much sign of it yet.
1
2
Sounds like is thinking along similar lines (twitter.com/pcwalton/statu)
All said, this doesn't seem to help with his original question. Instead, it seems to redouble the "worthless" feeling he mentions.
Are there creative solutions here to show the value?
Quote Tweet
Replying to @jntrnr @brendanzab and 2 others
It’s mostly an economic problem, IMO. Most software can’t afford to spend developer time/expertise on proving correctness. The software that *can* afford it tends to be core infrastructure, because it’s widely depended on.
2
Well, to the original question, I’d answer: Focus on the niche of widely-used, core infrastructure code where the cost of a bug is really high. Ignore Web apps and so forth (for now, anyway).
Prove your filesystem driver correct, or your malloc implementation, etc.
2
5
Agree with . Niches for DT languages are "well defined infrastructure, very expensive when wrong, very hard to be sure when right". I.e. places they're already growing! Compilers, kernels, crypto, consensus, filesystems. But they do need to emit fastish (final) products.
1
1
3
(Indeed as mentions re: Hofmann's work -- and his own -- there's space for stating and proving arbitrarily-precise properties of the _resource usage_ of a program in the types of a suitable DT system. Not the only horse in the race, but a promising application.)
1
4
I don't know if I agree with your premise - it's possible that I'm just part of a small bubble, but I have found that many programmers are becoming more and more interested in types-as-contracts
2
1
I agree there's a growing audience. I just think it's very, very far from mainstream. And that's 100% ok; I took 's initial tweet as light, self-deprecating sarcasm. Mainstream is still dynamic JS/Python/PHP/R/ObjC plus a few moderately-typed things like Java/C#/Swift.
2
To be clear here: the interesting types I've seen people write in DT systems are things like "a time-slicing kernel that preserves sequential semantics of the programs it is scheduling" or "a multiprecision-integer implementation of scalar multiplication within an elliptic curve"
2
4
Those applications are all well and good, but is definitely committed to a vision for dependent types in which they make all kinds of programming _easier_, rather than being just about proving correctness.
1
4
Yes, definitely! Just like regular types don’t just have to be about correctness all the time. It’s a harder thing to quantify though, similar to hoe it is in dynamic/static debates.