Thanks, while short, it sure looks interesting. SPARK statically checked function pre- and postconditions and constrained types certainly look very interesting

Thanks, while short, it sure looks interesting. SPARK statically checked function pre- and postconditions and constrained types certainly look very interesting especially for embedded systems. And for a lot of other low level code as well.