Ada SPARK is better than dependent types

http://electronicdesign.com/test-measurement/requiem-bug-verifying-software-part-2-formal-verification-through-spark-2014

>>2
No, that's not an argument.

SPARK is better because it can prove more safety statically, with less Peano numerals bullshit.

For example, no dependently typed language I know of can tell you that

Split := (Left + Right) / 2;

is actually a bug.