"Strong typing vs. strong testing"

[Keith Thompson]

RG <rNOSPAMon at flownet.com> writes:
> In article <lnk4m45eu0.fsf at nuthaus.mib.org>,
>  Keith Thompson <kst-u at mib.org> wrote:
>
>> RG <rNOSPAMon at flownet.com> writes:
>> > In article 
>> > <07f75df3-778d-4e3d-8aa0-fbd4bd108a57 at k22g2000prb.googlegroups.com>,
>> >  Squeamizh <squeamz at hotmail.com> wrote:
>> >> On Sep 29, 3:02 pm, RG <rNOSPA... at flownet.com> wrote:
>> [...]
>> >> > This is a red herring.  You don't have to invoke run-time input to
>> >> > demonstrate bugs in a statically typed language that are not caught by
>> >> > the compiler.  For example:
>> >> >
>> >> > [ron at mighty:~]$ cat foo.c
>> >> > #include <stdio.h>
>> >> >
>> >> > int maximum(int a, int b) {
>> >> >   return (a > b ? a : b);
>> >> >
>> >> > }
>> >> >
>> >> > int foo(int x) { return 9223372036854775807+x; }
>> >> >
>> >> > int main () {
>> >> >   printf("%d\n", maximum(foo(1), 1));
>> >> >   return 0;}
>> >> >
>> >> > [ron at mighty:~]$ gcc -Wall foo.c
>> >> > [ron at mighty:~]$ ./a.out
>> >> > 1
>> >> >
>> >> > Even simple arithmetic is Turing-complete, so catching all type-related
>> >> > errors at compile time would entail solving the halting problem.
>> >> >
>> >> > rg
>> >> 
>> >> In short, static typing doesn't solve all conceivable problems.
>> >
>> > More specifically, the claim made above:
>> >
>> >> in C I can have a function maximum(int a, int b) that will always
>> >> work. Never blow up, and never give an invalid answer.
>> > 
>> > is false.  And it is not necessary to invoke the vagaries of run-time 
>> > input to demonstrate that it is false.
>> 
>> But the above maximum() function does exactly that.  The program's
>> behavior happens to be undefined or implementation-defined for reasons
>> unrelated to the maximum() function.
>> 
>> Depending on the range of type int on the given system, either the
>> behavior of the addition in foo() is undefined (because it overflows),
>> or the implicit conversion of the result to int either yields an
>> implementation-defined result or (in C99) raises an
>> implementation-defined signal; the latter can lead to undefined
>> behavior.
>> 
>> Since 9223372036854775807 is 2**63-1, what *typically* happens is that
>> the addition yields the value 0, but the C language doesn't require that
>> particular result.  You then call maximum with arguments 0 and 1, and
>> it quite correctly returns 1.
>
> This all hinges on what you consider to be "a function maximum(int a, 
> int b) that ... always work[s] ... [and] never give[s] an invalid 
> answer."

int maximum(int a, int b) { return a > b ? a : b; }

>           But if you don't consider an incorrect answer (according to 
> the rules of arithmetic) to be an invalid answer then the claim becomes 
> vacuous.  You could simply ignore the arguments and return 0, and that 
> would meet the criteria.

I don't believe it's possible in any language to write a maximum()
function that returns a correct result *when given incorrect argument
values*.

The program (assuming a typical implementation) calls maximum() with
arguments 0 and 1.  maximum() returns 1.  It works.  The problem
is elsewhere in the program.

(And on a hypothetical system with INT_MAX >= 9223372036854775808,
the program's entire behavior is well defined and mathematically
correct.  C requires INT_MAX >= 32767; it can be as large as the
implementation chooses.  In practice, the largest value I've ever
seen for INT_MAX is 9223372036854775807.)

> If you try to refine this claim so that it is both correct and 
> non-vacuous you will find that static typing does not do nearly as much 
> for you as most of its adherents think it does.

Speaking only for myself, I've never claimed that static typing solves
all conceivable problems.  My point is only about this specific example
of a maximum() function.

[...]

-- 
Keith Thompson (The_Other_Keith) kst-u at mib.org  <http://www.ghoti.net/~kst>
Nokia
"We must do something.  This is something.  Therefore, we must do this."
    -- Antony Jay and Jonathan Lynn, "Yes Minister"