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


marcio

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