int nan

[Michiel Helvensteijn]

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