Static typing, as done in mainstream languages, doesn't show your program is correct. Is you compiler written in a mainstream language correct just because it compiles? Of course not. Don't point to academic curiosities with dependent types if they aren't actually used. Extensive testing, on the other hand, is used in the "real world" for assurance.