Well, there's a bit of a problem in how you're qualifying things. For example, certain things that aren't obviously handled by the type-system might be.

One example would be loops and off-by-one errors. For the case of For-loops on arrays Ada's solution arguably does so via the type-system; in Ada arrays "know" their own length, start- and stop-index and these are query-able via attributes.

So, given Function Sum( Input : Integer_Array ) return Long_Long_Integer you could for-loop on the parameter, querying the 'Range attribute -- yielding a possible implementation of:

Function Sum( Input : Integer_Array ) return Long_Long_Integer is Begin Return Result : Long_Long_Integer := 0 do For Index in Input'Range loop Sum:= Sum + Long_Long_Integer( Input(Index) ); End Loop; end return; End Sum;

And the entire problem is avoided via the type-system.

That is a reflection on which language you use. I prefer a language where a large majority of bugs are type-related. How about you?