[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[ih] PDP-11 high level language [Re: how big was the host file]
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
(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.