Optionally typed programming languages are still a big research area and we are just now starting to see some of that research go more mainstream, with things s

Optionally typed programming languages are still a big research area and we are just now starting to see some of that research go more mainstream, with things such as Typescript. That said, I don't expect to see a language that does all the things you listed at the same time, since type systems are all about tradeoffs between expressivity and complexity and there is an upper bound in how much complexity a programmer can handle. There are also a lot of other tradeoffs that you need to think about: do unproved assertions get converted to runtime checks or to compile errors? Can you implement that efficiently? How will type inference work? Is it OK to design an unsound type system? etc etc. I can give you some pointers if you want to look for something more specific.