🚀 go-pugleaf

Grier:
>   In mathematics, it makes NO sense to talk about applying a function
>or operation to a symbol unless the symbol is known to be in the
>domain of the operation/function.  I.e. writing something like "for all
>x, exp(x) is greater than zero" is nonsense.  exp's domain is commonly
>the reals, and may be extended to bigger domains like the complexes, but
>that doesn't mean it applies to the empty set, or the tree outside my
>house's door.  The correct way to write that would be, "for all x, if
>x is a real number, exp(x) is greater than zero."

Hmm... so what is the correct way of finding if x is a member of set
y?  What is the domain of a function which selects the first 5 from
an ordered sequence?  What is the domain of = (test-if-equal)?  What
is the domain of encapsulation (obtain-a-pointer-to)?  What is the 
domain of search (look-up-in-table)?

Why should I limit assignment (name-association) based on the domain
of, for instance, addition?

> ...
>  Now, that's the hard stance.  Following this philosophy, if x
>is in the set of integers, x is also NOT in the set of reals (a nice
>copy of it and the rest of the integers are embedded there.)  So,
>it's not uncommon to sleaze through your typing when there is a clear
>an unambiguous conversion implied.

And which of those types is the domain of log() ?  Can you think of a
good reason to not have runtime type-checking for log?

>|> Finally, to Mr. Grier, who posed the rhetorical problem about trusting
>|> software in critical systems which might have latent bugs:  would you
>|> really trust such software if it had never been tested?  Would it make
>|> you feel safer if each type of data required seperate chunks of code,
>|> with the associated tests and branches and variant storage mechanisms?
> 
>   Yes and no.  No first.
> 
>   "No", because that's why I think that subtyping and inheritance is
>so wonderful.  If there's an obvious way to specialize an operation to a
>subtype, it *is* clearer and still absolutely statically correct to apply the
>supertype's operation to a value of the subtype.

No this makes you feel safer?  Or no it doesn't make you feel safer?

>   "Yes", because otherwise you end up putting operations up artifically
>high in the tree.  The one which comes to mind and really burns me is 
>when there's a "Shape" type, and because people want to have values of
>type "Shape" and want to apply the "diameter()" operation to them.  Shapes
>don't all have diameters!  At least if they do, it's not with the implicit
>meaning implied by the C++ folks who want to define a diameter()
>virtual member function for Shape.

Sounds like a good reason to avoid testing to me.  (Right folks?)

>   My motivation is that I believe that compilers should try to do their
>best to ensure correctness of a program implementation before allowing 
>it to be executed.  If you don't believe in that, well, we differ and
>that's life. I just wouldn't do my banking or trust my life to software which
>relies on extensive testing rather than some level of ensurred correctness.

I have no objection to compilers doing their best.  Nor do I claim
that testing somehow negates the responsibility of the designer to
ensure correctness.  Nor do I claim that the compiler relieves the
designer of the responsibility for correctness. 

On the other hand, I do claim that IF the language lets me, I can
write programs which can be verified quite simply.  The technique is
very similar to induction.  (Check boundary conditions, check for
typical case).  Sometimes you can make your testing into a proof of
correctness (given basic assumptions about the correctness of the
underlying machinery).  Sometimes not.  

As an aside, you can test both your understanding of a concept, and
its correctness by implementing it and seeing if it works.  Proofs can
have bugs in them too, you know.

>   (I don't claim that compilers will ever be able to prove correctness
>of the semantics of an algorithm, but I'd like them to at least ensure the
>correctness of the proof/implementation.)

And how is a compiler supposed to prove that a program fulfills its
purpose?  At best, the compiler can prove that the program can be
compiled. 

>...
>   I don't WANT a smart computer, I don't WANT a computer which can
>misinterpret ambiguous commands, I don't WANT a computer which
>can forget.  (machine checks/hardware failures don't count.)

I do not believe I was arguing for any of these features.

>   I want a computer which does EXACTLY what I tell it, really fast.  If what
>I tell it to do doesn't or might not make sense, I want it to let me know
>so I can clear up any ambiguity as early as possible, rather than letting it
>find it out later (rush hour at a busy airport, suddenly over 256 planes are
>in the airspace, and some program writes past the end of an array, blasting
>away the stack, crashing the ATC computer,) or make some guess ...

A very good reason for runtime type checking.

>   This is tiring.  If you don't agree with me, that's OK, but I hope you
>stay in the research world rather than producing software which people
>pay for and expect to work reliably.  But if you're going to claim that
>this approach of dynamic typing increases {productivity, quality, 
>performance, correctness, robustness}, I'll continue to differ with you.

I must admit that following your line of thought (or attempting to--
I'm not sure I succeeded) is tiring for me as well.  I should point
out that I am not in the research world, and work very hard to see
that what people pay for works well.  And while I disclaim knowledge
of what you think dynamic typing is, I do claim that type as a
property of DATA as opposed to a property of a NAME does increase
productivity, quality, correctness as well as robustness.

In fact, I claim that assigning types to names, independent of the
assigned values, is a akin to side-effect driven programming.  I
realize that it is necessary at a low level.  I don't see it as a
productivity boost.  


Raul Rockwell