That same argument was--and sometimes still is--made about the type system in Rust. As someone who has been building a network core recently where a small amoun

That same argument was--and sometimes still is--made about the type system in Rust. As someone who has been building a network core recently where a small amount of dependent typing (more than I can pull off in C++, where the templating engine kind of hints in the right direction by letting you parameterize types over values) would go a long way, I personally feel like dependent typing could easily be added to existing languages, and the secret is to just make the fallback be to a runtime hard-enforced check (so it feels like something of a compiler optimization, though one where I would like to then be able to insist/check--even if only by using some external linting tool--that it is happening at compile time).