[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