[cap-talk] object-oriented-security.org

John R. Strohm strohm at airmail.net
Fri Mar 5 17:09:18 PST 2010

"Dirk Pranke" <dpranke at chromium.org> said:
> Something I've never seen in practice about this ... I understand and
> agree that global variables are bad, but
> I've never seen a programming language that actually completely avoids
> them. Granted, I've never actually
> studied actual E programs, but every other language seems to have some
> set that is provided by the linker.

Review the Gypsy Verification Environment work at UT Austin in the 1970s.  Gypsy 
was based on Pascal, was fully verifiable, and contained neither global 
variables nor GOTO statement.  It was designed from the ground up to be fully 
formally verifiable.  It did not even contain pointers, although the graduate 
students who were doing serious Gypsy programming, to demonstrate that serious 
programming COULD be done, and verified, found a way to do something similar.

It did contain concurrency.  Tasks were loosely-coupled, communicating through 
buffers (essentially semaphore-protected FIFO queues).

More information about the cap-talk mailing list