One observation from talking to industrial teams: PL has a lot of cool concepts that get lumped together into the same language or community, and industrial language designers then need to decouple them from features they don't want
Conversation
As an example, it seems like most people who want dependent types for practical programming actually don't care about soundness too much, they just want a helpful and very natural annotation system, basically
4
16
Very true! My colleague makes an analogy to the uncanny valley. Unsound but useful type annotations and complete soundness are both nice, but there's a pit in between where typing is sound enough that you rely on it, but unsound enough to allow nasty bugs in.
1
2
Getting a gradually-typed language across that valley while maintaining developer productivity is an interesting challenge for industrial language designers.
1
1
It seems like a fundamental need is the ability to say "I promise," much like Axioms in proof assistants, but with that being socially acceptable and with strong support, maybe even the default
1
3
Then for your power users, you can build soundness on top of that, by way of a plugin or something
1
1
Smells a bit like Rust's unsafe (aka. 'trusted') blocks! And the semantic soundness stuff from Rust Belt, where you can use Coq to prove your unsafe code is actually upholding Rust's guarantees.