[kaba0]

> implementation of dependent types, which is fine.

Which you have to prove, which is absolutely non-trivial. I guess it could be made into a runtime check as well where static analysis is not possible, but that seems to be a quite hard to reason about language regarding performance.

[mycall]

.NET Code Contracts has both compile time and runtime checks, although it always felt like a bolted on solution even though it is baked into the framework. I guess this is why it didn't carry forward into the .NET Core rewrite.