Hi, ri...@happyleptic.org skribis:
> What's of more practical importance to me is that when you > change a data structure somewhere you can be confident that the compiler > will spot every other places where your changes require other changes. > You have not this safety with Scheme, and this is much more problematic > ; again, in my experience. You have to run your code with all possible > inputs in order to make certain that you did not forget to propagate > your changes somewhere. Yes, you’re right. Having the compiler type-check parts of all your program is a win, no doubt about it. Nevertheless, type safety can be viewed as one of the many properties of a program one could want to prove or test. Did you know that Coq would only compile a function when it can prove that it terminates? That’s another kind of compiler-supported proof one quickly gets used to. Thanks, Ludo’.
