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