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) 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 [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer |
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 <[hidden email]> wrote:
_______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer |
Free forum by Nabble | Edit this page |