The things is that dynamically typed languages are easier to implement than statically typed languages. Static typing comes down to making statements about the program and deriving other statements from them. It leads to all sorts of interesting work including I think into systems like Z. However theorem provers are limited in what they can do, and it can be both limiting and a big distraction to you as programmer to get into a dialogue with the theorem prover about your program. It can distract you from your original intention which was to write a program to do something in particular.
So simply put, dynamic languages are better than static ones because they don't distract you with type discussions that can end up being unprofitable or limiting. Static languages are better because sometimes the type discussions lead to early and convenient detection of bugs and can also in some cases make it easier for other people to understand you program or how to use your library. Static types I think also help refactoring tools. Having optional typing in clojure is very nice. It allows for a lot of experimentation and research on type systems and for them to be used to the extent that people find them useful in their work. It is why I guess Alan Kay said that lisp is not a language, it's a building material. If you want to know what are the current problems in static typing you going to have to start learning what people are doing in that field, e.g. is their foreign function interface from Haskel to Java? Why not? Can a well typed program still exhibit bugs? If the type checking is so powerful why do bugs persist? You might also look at what Gilhad Brakka was attempting to do with newspeak and his notions of types being anti-modular. You are not going to find a proof that that line of enquirely is fruitless, you'll instead find what people can do today in that field and where they're pushing the bounds. regards, Richard. -- -- You received this message because you are subscribed to the Google Groups "Clojure" group. To post to this group, send email to clojure@googlegroups.com Note that posts from new members are moderated - please be patient with your first post. To unsubscribe from this group, send email to clojure+unsubscr...@googlegroups.com For more options, visit this group at http://groups.google.com/group/clojure?hl=en --- You received this message because you are subscribed to the Google Groups "Clojure" group. To unsubscribe from this group and stop receiving emails from it, send an email to clojure+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/groups/opt_out.
