Hal Abelson from MIT explains the difference of mindset at minutes 37-41 https://www.youtube.com/watch?v=Iib713oLFt4
On Sat, Oct 27, 2018 at 3:41 PM William Sit <[email protected]> wrote: > 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= > [email protected]> on behalf of Tim Daly <[email protected]> > *Sent:* Wednesday, October 17, 2018 1:01 PM > *To:* Tim Daly > *Subject:* [Axiom-developer] insight > > I think I finally understand why I keep asking stupid questions and > find 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. > We're using the same words but we don't mean the same thing. > > You are using types "ABOUT programming" and I'm using types > "about PROGRAMMING". > > You use types as a meta-language to talk ABOUT programs > and use type-erasure to eliminate them at runtime. When you say > a 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 mean > that the computed result is "correct" in that it agrees with what a > user 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 disjoint > disciplines 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 > >
_______________________________________________ Axiom-developer mailing list [email protected] https://lists.nongnu.org/mailman/listinfo/axiom-developer
