[plt-scheme] Re: to define, or to let

Bill Richter wrote:
> Vadim Nasardinov  <el-vadimo at comcast.net> responded to me:
...
>    You pack more knowledge into your software by being cognizant of
>    the evaluation order dependencies or lack thereof.
>
> But it might be false knowledge!  Until the Mzscheme compiler can
> enforce "lack thereof", I think MF will say this is unsafe.

Bill, you're getting yourself into a Rumsfeldian dilemma, worrying about
what  are known knowns to someone else.  You should be worrying about your
own knowns and unknowns first.

The false knowledge you're concerned about is no different than a piece of
code that contains false knowledge about types.  The MzScheme compiler
does not enforce that.  There are also all sorts of other things that are
encoded in code, which compilers cannot check.  Real programs have many
kinds of bugs which can only be caught by testing.

All of the tools we use, like static type checks, runtime type checks,
contract checks, code reviews, test suites, alpha testers, and beta
testers, are designed to help us to either prove a lack of bugs, or detect
and find bugs when we can't prove their non-existence.  With static
checks, you're focusing on just one small aspect of that picture.

The fact that the compiler can't statically check order independence is
not a valid rationale for eliminating the ability to assert it.  That's
like saying "we hardly ever catch car thieves anyway, so let's just take
that pesky vehicle theft law off the books so we aren't constantly
reminded of our shortcomings".

This is playing a game with systems, saying you don't know how to deal
with something in the very specific way you want to deal with it, so you
define the system so that you can't express that thing in it.  But Goedel
is watching you, and wondering why you didn't pay more attention in that
Foundations of Mathematics course.  Your game doesn't eliminate the entire
problem, it just makes it harder to talk about it within the system, like
a dysfunctional family.

Besides, skipping back a metaphor, people can use tools like LoJack to
make car theft easier to fix.  That won't help as much after the law's
been eliminated.  "Hey, that guy stole my car!"  "Yeah, but that's not
against the law."  Suddenly, people are stealing cars left and right, and
there's nothing you can do about it, other than obsessively follow your
car's blip on the LoJack tracking screen, or maybe hire Vinnie from
Brooklyn (buddy of mine) to get your car back.

It's that moral hazard I was talking about.  Make depending on eval order
OK everywhere, and people will do it everywhere.  May as well be
programming in Python.

> Let me re-ask: Aren't Robbie's contract.ss enforced by DrScheme?

They're enforced by Robby's contract.ss.  Anyone else can write things to
enforce their own contracts, too.  That's the cool thing about macros. 
Like BrBackwards (which is just a tad less comprehensive than Robby's
stuff).

> Or a real dumb question.  Typing is a way to "pack more knowledge into
> your software".  That's a weakness of Scheme compared to ML.

It's a tradeoff, i.e. there are weaknesses in both directions.

> But doesn't ML enforce typing?  Reaally dumb question: C enforces
> typing, doesn't it?  If a function is declared to take integer
> arguments, and you call it with a float, the compiler flags you,
> right?

Yes.  Those are static checks.  So what?  Not even C or ML can check
everything statically.

Anton