[touisteur]

Two of the most interesting things that trickled down during the design of Spark2014:

1- contracts are written in the same language as the code to be checked/proved. This made important to add expressive features to the language (for all / for some: quantifiers! expression functions, if- and case-statements and more recently the new delta-aggregates notation): these additions make the language far more expressive without too much loss of readability.

2- executable contracts: most contracts can be checked at runtime or proved. And the escape hatch (code only present for proof) is 'ghost' code which is also a nice addition.

Lots of little nifty additions to the language, from just 'thinking in contracts' or 'designing for probability'.