Re: Vectors as functions

[Shriram Krishnamurthi <address@hidden>]

To correct something I've repeatedly seen mentioned in this thread:

There are many more uses for first-orderness, and more broadly for
restricting the power of programmer, than *optimization*.  These
restrictions are also necessary to build an effective form of
reasoning and verification engine (starting with a type checker and
moving on up the validation food chain).

The same things that make it hard to optimize also make it hard for
tools to reason about programs.  And one could argue, loosely, that
things that make it hard for programs to reason about programs also
make it hard(er) for humans to reason about them.  So the costs are
manifold, and improvements in speed are only a part of that --
arguably even a very small part.

[In fact, you don't even need to get so fancy as "verification".
 Consider a tool like Check Syntax in DrScheme, which draws overlays
 arrows atop the source from binding to bound instances of variables.
 If you can't tell what the binding structure is without running the
 program, and if that structure can potentially change every time you
 run your program, what hope does Check Syntax have?  And, by
 extension, what are the odds the programmer can tell?]

Therefore, those of us in the verification business care deeply about
finding reasonable restrictions to place on the power of programmers.
In practice, this means finding a sweet spot that is neither so low in
abstraction that it reveals no structure (eg, Turing machine) nor so
high in abstraction that it hides all structure (by making it too
difficult to determine control flows, binding structures, etc).

We now return you to your regularly scheduled show about whether
numbers should be treated as functions.

Shriram