checkedint call removal

[bearophile via Digitalmars-d]

Ola Fosheim Grøstad:

> 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

I have started to read those pages, it looks interesting. From 
one of the first links (Sudoku solver):


valid values are 0..9. 0 denotes an empty cell

   predicate valid_values (g:grid) =
     forall i. is_index i -> 0 <= g[i] <= 9


So can't they represent that the value 0 is an empty cell in the 
code instead of comments? (I think this is possible in Ada 
language).

It's a bit sad that D1 has removed the literate programming 
feature of D1. In Haskell it's used all the time.

Bye,
bearophile