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

*To*: address@hidden*Subject*: Re: Vectors as functions*From*: Shriram Krishnamurthi <address@hidden>*Date*: Fri, 15 Aug 2003 19:26:06 -0400*In-reply-to*: <200308152107.h7FL7qg19917@orchestra.cs.caltech.edu>*References*: <20030814170153.80D4B6BEDE@laime.cs.uchicago.edu><AA236D25-CEA2-11D7-B 291-0003938EB888@web.de><16188.3934.267729.188080@cs.brown.edu><32783.141.154.13.159.1060907724.squirrel@stuff.hrnoc.net><200308150336.h7F3aErQ208596@pimout5-ext.prodigy.net><200308150440.h7F4eEW32071@orchestra.cs.caltech.edu><y9lfzk2lwm7.fsf@informatik.uni-tuebingen.de><200308151658.h7FGwCr15280@orchestra.cs.caltech.edu><nm9y8xuiygs.fsf@scrubbing-bubbles.mit.edu><200308151830.h7FIU7p17300@orchestra.cs.caltech.edu><039201c36363$8c931f30$8c730a81@Rasputin><200308152107.h7FL7qg19917@orchestra.cs.caltech.edu>*Sender*: 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

**Follow-Ups**:**Re: Vectors as functions***From:*mike@newhall.net

**Re: Vectors as functions***From:*James McCartney <asynth@io.com>

**References**:**Re:***From:*Robby Findler <robby@cs.uchicago.edu>

**Vectors as functions***From:*Shriram Krishnamurthi <sk@cs.brown.edu>

**Re: Vectors as functions***From:*mike@newhall.net

**Re: Vectors as functions***From:*Robby Findler <robby@cs.uchicago.edu>

**Re: Vectors as functions***From:*Michael Vanier <mvanier@cs.caltech.edu>

**Re: Vectors as functions***From:*Michael Sperber <sperber@informatik.uni-tuebingen.de>

**Re: Vectors as functions***From:*Michael Vanier <mvanier@cs.caltech.edu>

**Re: Vectors as functions***From:*Bruce Lewis <brlewis@alum.mit.edu>

**Re: Vectors as functions***From:*Michael Vanier <mvanier@cs.caltech.edu>

**Re: Vectors as functions***From:*"Joe Marshall" <jrm@ccs.neu.edu>

**Re: Vectors as functions***From:*Michael Vanier <mvanier@cs.caltech.edu>

- Prev by Date:
**Re: Vectors as functions** - Next by Date:
**Re: Vectors as functions** - Previous by thread:
**Re: Vectors as functions** - Next by thread:
**Re: Vectors as functions** - Index(es):