Nick Sabalausky wrote: > Init, assert, spell-check land, etc.
We're agreed. >>> Also, keep in mind that while, under this mechanism, it is certainly >>> possible for a coder to cause bugs by always knee-jerking the value to >>> zero whenever the compiler complains, that's also a possibility under >>> the "holy grail" approach. >> >> That's true. But if we did have the grail, the compiler would also be >> able to see that knee-jerking 'i' would not satisfy the contract of the >> outer function. >> > > No, it wouldn't, because it would have no way of knowing that's a > knee-jerk fix for a "using uninited var" error. But maybe I misunderstand > you? I mean that if the programmer has provided a postcondition of the outer function (the function that contains the variable 'i'), a verifying compiler will be able to give an error if knee-jerking 'i' results in a subtle bug in the function; one that would invalidate the postcondition. Of course, if no postcondition is supplied, the compiler can only assume you meant for exactly that thing to happen. The bug becomes a feature. :-) Anyway, the verifying compiler is a project I'm working on. I'm designing a language based on the assumption that compilers will become more and more sophisticated in the area of static analysis. Contracts are the most important feature of this language and assertions even have their own syntax (because they'll be used so much). Where the correctness of a piece of code cannot be proved at compile-time, a managed runtime environment is used. This offers the guarantee that the current state will always satisfy the contract. Assertions cannot be 'caught' and discarded. Many optimizations may also be based on contracts. It's a really fun project. -- Michiel Helvensteijn
