I've always felt comfortable programming in Lisp or Python, and I don't seem to miss strong typing very much. While programming Java though, with it's extensive

I've always felt comfortable programming in Lisp or Python, and I don't seem to miss strong typing very much. While programming Java though, with it's extensive library of functions, the more intelligent autocompletion provided by my IDE is very welcome. So I see both sides of the points being made here, but I do have a question for those HN readers that are closer to research in program correctness than I am. Why are types beleived to be so useful in insuring that programs express the intent of the programmer? It seems to me, that types are useful for useful for expressing the boundaries of components, but they seem rather awkward constructs to be wrestled with to express the invariants and predicates about the state of the program that I invariably end up using in my head to insure that my code is correct. For example, one might simply want to insure that three variables, say x, y and z, satisfy the relation (x <= y && y <= z) while inside a loop. The x, y and z might be integers or account-numbers or zip-codes or anything else with the <= predicate. What I want is not to twist the type system around to say that just while in this loop the type guarantees that (x <= y && y <= z). What I want in a programming language is to be able to express this as a claim I'm making about the program at this point and to have help from an interactive theorem prover that it is so. I'd expect some sort of dialog with my tooling that would point out where I needed to make changes to guarentee this or to indicate that it is a claim stronger than needed for the program to run correctly (and satisfy it's specifications). Type systems just don't seem very natural for this; I would think we would use something like Dijkstra's weakest-preconditions or temporal logic over program states. I really am asking for help in understanding where research on programming correctness is currently headed. (You don't have to explain it like I'm a fifth grader, I've been programming for 50 years, many in grad school.)