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=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!nntp-feed.chiark.greenend.org.uk!ewrotcd!newsfeed.xs3.de!io.xs3.de!news.jacob-sparre.dk!franka.jacob-sparre.dk!pnx.dk!.POSTED.rrsoftware.com!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: some trivial questions?
Date: Wed, 22 Nov 2017 18:15:41 -0600
Organization: JSA Research & Innovation
Message-ID: <ov53vd$ef3$1@franka.jacob-sparre.dk>
References: 
 <6a5368c5-f015-4dcb-9291-e77b40fa1bf1@googlegroups.com><ff607ea1-9d64-441b-b5e6-1a4377a5a199@googlegroups.com><oteku0$ek3$1@gioia.aioe.org>
 <oulbpm$p2t$1@franka.jacob-sparre.dk><oum6qv$1bdr$1@gioia.aioe.org>
 <ouo1hg$fjr$1@franka.jacob-sparre.dk><ouotuh$1ig3$1@gioia.aioe.org>
 <ouvjfp$8rd$1@franka.jacob-sparre.dk><ov0v0f$663$1@gioia.aioe.org>
 <ov2hvr$i7m$1@franka.jacob-sparre.dk> <87mv3fdsi3.fsf@nightsong.com>
Injection-Date: Thu, 23 Nov 2017 00:15:42 -0000 (UTC)
Injection-Info: franka.jacob-sparre.dk;
 posting-host="rrsoftware.com:24.196.82.226";
	logging-data="14819"; mail-complaints-to="news@jacob-sparre.dk"
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2900.5931
X-RFC2646: Format=Flowed; Original
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.7246
Xref: feeder.eternal-september.org comp.lang.ada:49079
Date: 2017-11-22T18:15:41-06:00
List-Id: <comp.lang.ada>

"Paul Rubin" <no.email@nospam.invalid> wrote in message 
news:87mv3fdsi3.fsf@nightsong.com...
> "Randy Brukardt" <randy@rrsoftware.com> writes:
>> Of course, a true proof is hard to do when the rules are primarily 
>> modeled
>> in English as opposed to some formal system.
>
> I'm surprised Ada doesn't have a formal semantics.  Maybe that's
> something that should be fixed?

That was attempted during Ada 9x, but the problem was that there was no way 
for normal humans to see if the formal semantics in fact properly modeled 
the language. Only the authors actually understood the formal model.

Creating a model that both formal and understandable by a run-of-the-mill 
language lawyer and finding volunteers to create the model seems unlikely 
(to say the least).

                                            Randy.