[ih] PDP-11 high level language [Re: how big was the host file]

[Karl Auerbach]

On 2/6/20 11:31 AM, Brian E Carpenter via Internet-history wrote:

>> Our compiler for the PDP-11 high level language ran on 6700
> 
> What was that? Which language and which compiler?

At SDC in the mid-to-later 1970's we created a Pascal-to-C compiler that 
we used to build our "verified secure" operating system for several 
sizes of PDP-11.

I put quotes around "verified secure" because our security criteria was 
fairly simple - the good ol' *-property (star-property).  And our proof 
was done by highly structured code (as demanded by our verification 
folks, Val Schorre, John Scheid (sp), and Marv Schaeffer) with clearly 
articulated assertions about side effects.

We trusted the C compiler and the underlying hardware to do the right 
things.

(Our OS design was one that used software capabilities; we were building 
machines with hardware capabilities for the next generation.)

Unfortunately the documents about what we did are still not easily found 
on the net.  I'm kicking myself for not retaining a copy of a paper I 
wrote about debugging a secure capability based operating system.

	--karl--