guile-user
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: A bit further toward the flamewar


From: Ludovic Courtès
Subject: Re: A bit further toward the flamewar
Date: Thu, 13 Oct 2011 23:14:01 +0200
User-agent: Gnus/5.110018 (No Gnus v0.18) Emacs/24.0.90 (gnu/linux)

Hi,

address@hidden 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’.




reply via email to

[Prev in Thread] Current Thread [Next in Thread]