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/p

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'.