"Verification Corner" videos, contract programming

[bearophile]

deadalnix:

> I wonder what is the method used by the compiler to ensure most 
> of the check at compile time.

It uses Z3 and Boogie:
http://rise4fun.com/

Bye,
bearophile