🚀 go-pugleaf

In article <1758@culhua.prg.ox.ac.uk> I wrote:

>  I'm not sure what you think is the design flaw: the programs in question
>  are not guaranteed to work (by the occam2 Reference Manual).  The only
>  `unexpected' behaviour is that Inmos' occam2 compiler happens to produce
>  code which makes this invalid non-program do what its author expected in case
>  the communication is on hard channels.  It is _very_ hard to guarantee that
>  all incorrect programs do something unexpected; the usual contract with a
>  language implementor is that all correct programs should only do the
>  expected.

In article <1991May20.113104.25938@rodan.acs.syr.edu> greeny@top.cis.syr.edu (Jonathan Greenfield) replies:

>  A secure language implementation detects any violation of the language
>  definition, either at compile-time, or at run-time.  If a language cannot be
>  implemented in a secure manner, then the language design is flawed.  If a
>  language can be implemented in a secure manner, but a particular system fails
>  to do so, then the system design is flawed.

But, but, but, come now.  Declaring a `CHAN OF ANY' gives the implementation
the right to assume that the programmer is going to use the channel properly.
That is what it says in the manual.  It is just like all the odd pragmas in
other languages (like those for turning off array bounds checks*) which you use
to assert to the compiler that _you_ the programmer will take responsibility
for guaranteeing a property which the compiler would otherwise be obliged to
check.  If you didn't want to make that guarantee, you didn't ought to have
declared the CHAN OF ANY.  

		( *  I don't know what the equivalent is for C programmers,
		     nor quite how to explain to C programmers what array
		     bounds checks are.					    )

The implementation can only be `secure' in the sense that it implements the
language as defined.  In any non-trivial language with while loops, you
will never get a mechanical guarantee from the compiler that the program
terminates.  In the same way, in any dialect of occam with CHAN OF ANY,
you will not get a mechanically checked guarantee of proper channel use.
And serve you right.  Of course, you might want a compiler for particular
applications to reject CHAN OF ANY declarations, but then it wouldn't be
an occam2 compiler, would it?
									g