Chris Smith <[EMAIL PROTECTED]> writes: > I thought about this in the context of reading Anton's latest post to > me, but I'm just throwing out an idea. I think there is some sense of convergence here. In particular, I reason about my program using "unsound types". That is, I reason about my program using types which I can (at least partially) formalize, but for which there is no sound axiomatic system. Now, these types are locally sound, i.e. I can prove properties that hold for regions of my programs. However, the complexity of the programs prevent me from formally proving the entire program is correct (or even entirely type-safe)--I generally work in a staticly, but weakly-typed language. Sometimes, for performance reasons, the rules need to be bent--and the goal is to bend the rules, but not break them. At other times, I want to strenghten the rules, make parts of the program more provably correct. How does this work in practice? Well, there is a set of ideal types, I would like to use in my program. Those types would prove that my program is correct. However, because there are parts of the program that for perfomnace reasons need me to widen the ideal types to something less tight, pragmatic types. The system can validate that I have not broken the pragmatic types. That is not tight enough to prove the program correct, but it provides some level of security. To improve my confidence in the program, I borrow the tagging concept to supplement the static type system. At key points in the program I can check the type tag to ensure that the data being manipulated actual matches the unprovable ideal type system. If it doesn't, I have a witness to the error in my reasoning. It is not perfect, but it is better than nothing. Why am I in this state, because I believe that most interesting programs are beyond my ability to formally prove them, or at least prove them in "reasonable" time bounds. Therefore, I prove (universally quantify) some properties of my programs, but many other (and most of the "interesting") properties, I can only existentially quantify--it worked in the cases that it was tested on. It is a corrolary of this, that most programs have bugs--places where the formal reasoning was incomplete (did not reason down to relevant interesting property) and the informal reasoning was wrong.
Thus, the two forms of reasoning, static typing to check the formal properties that it can, and dynamic tagging to catch the errors that it missed work like a belt and suspenders system. I would like the static type system to catch more errors, but I need it to express more to do so, and many of the properties that are interesting require n-squared operations to validate. Equally important, the dynamic tags help when working in an essentially untrustworthy world. Not only do our own programs have bugs, so do the systems we run them on, both hardware and software. Moreover, alpha radiation and quantum effects can change "constants" in a program (some of my work has to do with soft-error rates on chips where we are trying to guarantee that the chip will have a reasonable MBTF for certain algorithms). That's not to ignore the effects of malware and other ways your program can be made less reliable. Yes, I want a well-proven program, but I also want some guarantee that the program is actually executing the algorithm specified. That requires a certain amount of "redundant" run-time checks. Knuth had a quote about a program only being proven and not tested that reflects the appropriate cynicism. I consider any case where a program gives a function outside of its domain a "type error", because an ideal (but unacheivable) type system would have prevented it. That does not make all errors, type errors, because if I give a program an input within its domain and it mis-computes the result, that is not a type error. -Chris -- http://mail.python.org/mailman/listinfo/python-list