People from the group developing Spec# at Microsoft Research finally published an article on their new Code Contracts approach.
Chosen excerpts: “embedding of contracts as code is a better approach”; “The language of conditions is just the language of expressions in the programming language used”; “ForAll and Exists that work over integer ranges and collections”; “Any methods called from within contract expressions should be pure methods”; “Runtime contract checking is particularly effective in conjunction with automated testing”; “generating good documentation from the embedded contracts is a key scenario”.
And the conclusion: “Since contract expressions are compiled by the existing compiler, the typical problem of having the specifications and the code drift apart due to edits, refactoring, etc., is avoided.”
All of this supports the vision of project Hi-Lite, and provides valuable experience reports which should inspire us in Hi-Lite.