Re: checkedint call removal

[via Digitalmars-d]

Here is a set of examples of annotated programs that have been 
formally proved correct for those interested:

http://toccata.lri.fr/gallery/why3.en.html
The advantage of formally separating what is proven from what is 
to be proved is quite obvious. You can generate annotated 
bindings for libraries and frameworks that can both increase 
correctness and provide semantic information that can be relied 
on (for optimization and other purposes).