The case for NaN

Richard (Rikki) Andrew Cattermole richard at cattermole.co.nz
Mon Jul 6 02:21:12 UTC 2026


On 06/07/2026 7:08 AM, Walter Bright wrote:
> On 7/5/2026 1:37 AM, Richard (Rikki) Andrew Cattermole wrote:
>> What we are able to do here though is throw static analysis at the 
>> problem: https://github.com/dlang/dmd/blob/master/changelog/ 
>> dmd.fastdfa.uninitialized.dd
> 
> 
> Static analysis cannot solve the problem 100%. It's the ole' halting 
> problem.

20 years ago yeah.

But today it is considered solved in the sense that we do have static 
analyzers that are sound that catch it.

https://www.nist.gov/publications/sate-vi-report-bug-injection-and-collection

See 6.2.4.7 and 6.4.3. "Both Astrée and Frama-C with Eva satisfied the 
SATE VI Ockham Sound Analysis Criteria."

-----------

However to solve this in D fully, isn't that hard, and we can make some 
minor sacrifices in false positives to make it a good experience.

Due to D being based upon the type state initialized, to downgrade to 
uninitialized, you must opt-out of it and into uninitialized. In other 
words annotate. This removes inter-procedural analysis as a requirement.

By eliminating uninitialized into global, and field, you can remove 
whole program analysis.

By using separation logic (paper published in 2002 hintity hint), you 
can model the indirection and fields.

https://en.wikipedia.org/wiki/Separation_logic

Throw in chaotic iteration, easy peasy to solve.

Of course I'm not saying that we need to solve it, due to there being 
some time cost involved, but its not the halting problem!



More information about the Digitalmars-d mailing list