ESC/Modula3 (Extended Static Checking) for D?

[Marcio]

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