Some early Lisps had both compiled and interpreted mode, where the interpreter used dynamic scoping and the compiler used lexical scoping. (Which, I presume, c

Some early Lisps had both compiled and interpreted mode, where the interpreter used dynamic scoping and the compiler used lexical scoping. (Which, I presume, caused much developer confusion when code worked fine in the interpreter and got very strange behavior once compiled.) Something analogous (but more sane) could be done with type systems. I'm very much a fan of strong static typing, but I understand the appeal of dynamic typing, particularly for small scripts and/or prototypes. Static type checkers (for most languages) are pretty simple theorem provers. For statically typed languages, the compiler (or, I suppose in rare cases, interpreter) rejects any program that it can't prove is free of type errors. An alternative would be to only reject programs that provably contain type errors. The difference in allowed programs covers the cases where the type checker can't prove either way. So, I'd love a language with a type checker that when ahead-of-time compiling code would refuse to emit libraries/binaries when it couldn't statically prove types were used correctly. In interpreted mode, it would only refuse to load code that it could statically prove contained type errors. Maybe when used within an interactive session, it would still allow (but warn) when code provably has type errors. As an added bonus, static type guarantees open up more opportunities for the optimizer. A single language offering some range of static guarantees would reduce the number of cases where dynamically typed code gets re-written into a higher performance statically typed language when re-factored into libraries. If you prefer, go ahead and dynamically type your scripts, etc. However, if/when it comes time to package up parts of your program for wider re-use as libraries, please tighten up the static guarantees of type safety.