|
From: | Tim Daly |
Subject: | Re: [Axiom-developer] insight |
Date: | Sat, 27 Oct 2018 20:27:58 -0400 |
The number of English words is finite, whereas the number of human ideas is infinite. So words are recycled to refer to different ideas in different contexts. Questions are NOT stupid. Clarification is crucial.
This happens in physics and mathematics, terms like integrals, integrable or integrability, constants, symmetry all have loaded meanings. Even in Axiom, overloading (or polymorphisms) are common. So what exactly does "addition" or the symbol + refer to? That is not a stupid question at all.
Relax, and keep asking!
William
William Sit
Professor Emeritus
Department of Mathematics
The City College of The City University of New York
New York, NY 10031
homepage: wsit.ccny.cuny.edu
From: Axiom-developer <axiom-developer-bounces+wyscc=address@hidden> on behalf of Tim Daly <address@hidden>
Sent: Wednesday, October 17, 2018 1:01 PM
To: Tim Daly
Subject: [Axiom-developer] insight"about PROGRAMMING".You are using types "ABOUT programming" and I'm using typesWe're using the same words but we don't mean the same thing.I think I finally understand why I keep asking stupid questions andfind statements in class so strange.
"You keep using that word.
I do not think it means what you think it means"-- inigo Montoya 1987 (in The Princess Bride)It is like an artist (programmer) taking an art theory class.
You use types as a meta-language to talk ABOUT programsand use type-erasure to eliminate them at runtime. When you saya program is "correct", you mean "type correct". So a 'plus' function(\x:nat \y:nat 7) which always returns 7 is still "type correct".
I use types as first-class objects that I can create, modify, and
pass around at run time. When I say a program is "correct" I meanthat the computed result is "correct" in that it agrees with what auser would expect.
The insight is that we are using the same words but different meanings.This may be why computer algebra and proof theory seem to be disjointdisciplines in computational mathematics.
The upside is that I'll finally stop asking stupid questions. Well,maybe not, as I seem to have a genius for generating them :-)
Tim
[Prev in Thread] | Current Thread | [Next in Thread] |