ESC/Modula3 (Extended Static Checking) for D?

[pragma]

Marcio wrote:
> 
> Spec# http://research.microsoft.com/specsharp/ does extra checks 
> (basically covers/solves the issues on slide 29 of 
> http://www.cs.princeton.edu/~dpw/popl/06/Tim-POPL.ppt ) thanks to 
> Simplify http://research.microsoft.com/specsharp/simplify.htm.
> 
> Simplify is the beast behind it, from ESC/Modula3 
> http://ftp.digital.com/pub/compaq/SRC/research-reports/abstracts/src-rr-159.html 
> 
> 
> I would like to suggest that it would be great if the D compiler 
> incorporated such an idea.
> 
> Even Haskell people seem to be doing it 
> http://lambda-the-ultimate.org/node/1689

I was curious, so I went looking for information. I found the following 
a little more enlightening:

(From the digital.com site above)
"The paper describes a mechanical checker for software that catches many 
common programming errors, in particular array index bounds errors, nil 
dereference errors, and synchronization errors in multi-threaded 
programs. The checking is performed at compile-time. The checker uses an 
automatic theorem-prover to reason about the semantics of conditional 
statements, loops, procedure and method calls, and exceptions. The 
checker has been implemented for Modula-3. It has been applied to 
thousands of lines of code, including mature systems code as well as 
fresh untested code, and it has found a number of errors."

My $0.02:

In short, I don't think there's any need to wait for Walter to implement 
this in DMD.

It would be one heck of an undertaking, but I honestly don't see why the 
DMD frontend can't be put to task here.  All it would take is someone 
who really had a firm grasp of the concepts outlined in the paper and 
used the frontend's parse-tree to perform the analysis.  You'd then have 
a separate tool that can grow and mature, apart from Walter's already 
burdened schedule.

- Eric