🚀 go-pugleaf

RetroBBS NetNews Server

Inspired by RockSolid Light RIP Retro Guy

Article View: comp.lang.misc
Article #1510

The Forbiden

#1510
From: David Gudeman
Date: Thu, 16 Aug 1990 19:17
76 lines
4171 bytes
In article  <6465@helios.ee.lbl.gov> austern@ux5.lbl.gov (Matt Austern) writes:
>In article <24043@megaron.cs.arizona.edu>, gudeman@cs (David Gudeman) writes:
>>I am always disturbed by the idea that for a language to have some
>>good property, it must forbid the programmer from doing X.
>
>I'm sure that this is obvious to everybody, but I think it bears
>repeating: if the "good property" is efficiency, this is often best
>achieved by forbidding the programmer from using certain
>constructions.

No, it is not obvious to me, and this idea is one that I was
specifically thinking about when I made my statement above.

>The more assumptions a compiler can make about a program, the better
>it can do the optimization, and in many cases, the only way a compiler
>can safely assume that a programmer doesn't do something is to make it
>illegal.

This is the assumption that I find obviously false.  Lets say that the
programmer is forbiden from doing X for efficiency reasons.  Then there
are three cases:

(1) the compiler verifies the property when compiling individual
modules.  If the compiler can verify that a property holds for a
program, then it can always use this information to decide whether to
do the optimization or not.  The programmer is given a choice between
using X and taking the efficiency hit, or not using X and getting the
same run-time performance as a language that forbids X.  You have lost
no performance, and you have gained expressiveness.

(2) the compiler/linker verifies the property at link-time, but you
want to do optimization at module compile time.  The compiler for the
extended language assumes that X is not used and generates code as
efficient as a language that forbids X.  But there is a special
declaration that tells the compiler not to make this assumption.
Again you have increased expressiveness at no penalty for those
programs that do not make use of the increased expressiveness.  The
compiler does not do the verification if the declaration told it that
X is used.

(3) the compiler does not verify the property at all.  As (2), except
for the verification.

Using your example:
>
>(The C calling convention is more complicated than the
>FORTRAN calling convention, for example, because C allows recursion.

Add to FORTRAN a procedure declaration that says a given routine may
be recursive.  Then the compiler uses the more complicated calling
convention for those routines only.  I suspect that FORTRAN is not
required to verify non-recursiveness, so this is a case (3), where the
compiler just trusts the user.  This however is _no different_ than
the current status, where the compiler must trust the user not to
write recursive code.  This does not introduce new sources for error,
because it will not cause an error if a procedure is declared
recursive when it is not.

>Can you really imagine a C compiler/linker that can prove that a
>program has no recursive calls, and use a simpler calling convention
>for such programs?)

In the first place, this has no bearing on my thesis.  In the second
place, yes.  It's really quite trivial to prove that recursion is
impossible in most non-recursive programs.  The only programs where
non-recursion cannot be proven automatically are those which have a
recursive call in a section of code that will never be executed, but
where the compiler cannot prove that the code will never be executed.
Since such programs are almost guaranteed to be not what the
programmer intended, I feel confident in saying that non-recursion can
be automatically proven in correct non-recursive programs.
-- 
					David Gudeman
Department of Computer Science
The University of Arizona        gudeman@cs.arizona.edu
Tucson, AZ 85721                 noao!arizona!gudeman
Technical Details
Message-ID: <24279@megaron.cs.arizona.edu>
Path: arc1-ca.pugleaf.net!utzoo!utgpu!news-server.csri.toronto.edu!mailrus!uunet!wuarchive!cs.utexas.edu!asuvax!noao!arizona!gudeman

Show Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!utzoo!utgpu!news-server.csri.toronto.edu!mailrus!uunet!wuarchive!cs.utexas.edu!asuvax!noao!arizona!gudeman
From: gudeman@cs.arizona.edu (David Gudeman)
Newsgroups: comp.lang.misc
Subject: The Forbiden
Message-ID: <24279@megaron.cs.arizona.edu>
Date: 16 Aug 90 19:17:40 GMT
Organization: U of Arizona CS Dept, Tucson
Lines: 76