I really hope that in the future gradual typing and dependent types can come together into an ergonomic to use system where we can let the compiler check/enforc

I really hope that in the future gradual typing and dependent types can come together into an ergonomic to use system where we can let the compiler check/enforce proofs of correctness, but not require them. There's a ladder of correctness (simple type checks, unit tests, integration tests, proofs of different aspects of correctness) and each has a tradeoff vs effort. It would be really great to be about to be able to move around it without rewriting much code, but rather by adding more and more annotations as needed for your use.