It would be great if the language allowed you to defer choices and program like in Haskell and then add constraints later and end up with the advantages of Rust. Or apply a series of correctness preserving transformations (perhaps GPT can help with that).
