25 May
2024
25 May
'24
5:53 p.m.
On 5/25/2024 12:36 PM, Tom Perrine wrote:
Another Gypsy user here...
For KSOS-11 the kernel was described in SPECIAL - as a set of axioms and
theorems. There was no actual connection between the formal
specification in SPECIAL and the Modula code.
Some of the critical user-space code for a trusted downgrade program, to
bridge data from higher levels of classification to lower, was written
in Gypsy. I visited UT Austin and Dr Good(?)'s team to learn it, IIRC.
Gypsy was considered better in that the specification was tied to the
executable through the pre/post conditions - and the better support for
semi-automated theorem proving.
When I was transitioning from being a rock n' roller to computer science
student, I took my first undergraduate languages course from Don.
https://www.dignitymemorial.com/obituaries/austin-tx/donald-good-8209907
Charlie
--
voice: +1.512.784.7526 e-mail: sauer(a)technologists.com
fax: +1.512.346.5240 Web: https://technologists.com/sauer/
Facebook/Google/LinkedIn/Twitter: CharlesHSauer