From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: fac41,15edb893ef79e231 X-Google-Attributes: gidfac41,public X-Google-Thread: f4fd2,23202754c9ce78dd X-Google-Attributes: gidf4fd2,public X-Google-Thread: 103376,15edb893ef79e231 X-Google-Attributes: gid103376,public X-Google-Thread: 114809,15edb893ef79e231 X-Google-Attributes: gid114809,public X-Google-ArrivalTime: 2002-02-13 09:51:36 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!news-spur1.maxwell.syr.edu!news.maxwell.syr.edu!newsfeed.cwix.com!news.binc.net!kilgallen From: Kilgallen@SpamCop.net (Larry Kilgallen) Newsgroups: comp.lang.lisp,comp.lang.ada,comp.lang.eiffel,comp.lang.smalltalk Subject: Re: True faiths ( was Re: The true faith ) Date: 13 Feb 2002 11:51:26 -0600 Organization: LJK Software Message-ID: <65Wifyx6swV+@eisner.encompasserve.org> References: <4idg3u40ermnp682n6igc5gudp7hajkea9@4ax.com> <3219936759616091@naggum.net> <3c4a149d.9839580@news.bigpond.com> <43d7620c.0202130831.306d52d5@posting.google.com> NNTP-Posting-Host: eisner.encompasserve.org X-Trace: grandcanyon.binc.net 1013622693 2906 192.135.80.34 (13 Feb 2002 17:51:33 GMT) X-Complaints-To: abuse@binc.net NNTP-Posting-Date: Wed, 13 Feb 2002 17:51:33 +0000 (UTC) Xref: archiver1.google.com comp.lang.lisp:26444 comp.lang.ada:19971 comp.lang.eiffel:5669 comp.lang.smalltalk:19565 Date: 2002-02-13T11:51:26-06:00 List-Id: In article <43d7620c.0202130831.306d52d5@posting.google.com>, tshawke@qwest.com (Tom Hawker) writes: > If I remember correctly, Pascal was originally designed based on a > provability calculus. That is, Pascal programs were supposed to be > provably correct (don't ask me to define that), which is why there > were so many things "missing", such as C-equivalents "break" and > "goto". Provability gave way to usability... DEC's SVS project to provide an A1 Security Kernel on VAX was written in Pascal, with special caution taken to omit the Pascal runtime library DEC generally used, because that was written in a lower level language. This had to do with provability of the implementation. The project was dumped after going into Field Test because DEC found out there was no real customer demand. (NCSC wanted other agencies to use A1 systems, other agencies did not want to spend their money on that.)