An actual positive in my book. If you consider back propagation of constraining types wrt the derivative of developer effort you get smooth gradients. Program

An actual positive in my book. If you consider back propagation of constraining types wrt the derivative of developer effort you get smooth gradients. Program works and is correct, but developer gets yelled at by its IDE (IntelliJ does) until there's a proof of it to some degree. I wish that types and proofs were more progressive. For example in Java, why can't we have the compiler tell us what's missing for proving a variable does not escape and we have to wait runtime to see if we had the optimization? Sometimes we'd like to guarantee it, and not just get it opportunistically.