From: Victor Porton <porton@narod.ru>
Subject: Re: some trivial questions?
Date: Thu, 23 Nov 2017 02:19:09 +0200
Date: 2017-11-23T02:19:09+02:00 [thread overview]
Message-ID: <ov5463$1adm$1@gioia.aioe.org> (raw)
In-Reply-To: ov53vd$ef3$1@franka.jacob-sparre.dk
Randy Brukardt wrote:
> "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
Attempted in 90th?!
Which formal proof assistant was used?
> 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.
--
Victor Porton - http://portonvictor.org
next prev parent reply other threads:[~2017-11-23 0:19 UTC|newest]
Thread overview: 101+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-11-01 18:44 some trivial questions? tclwarrior
2017-11-01 19:55 ` Shark8
2017-11-01 20:03 ` Dmitry A. Kazakov
2017-11-01 21:30 ` Luke A. Guest
2017-11-06 22:43 ` Robert A Duff
2017-11-01 21:39 ` Jeffrey R. Carter
2017-11-02 1:19 ` tclwarrior
2017-11-02 3:04 ` Luke A. Guest
2017-11-02 4:19 ` gautier_niouzes
2017-11-06 22:52 ` Robert A Duff
2017-11-17 0:45 ` Randy Brukardt
2017-11-02 8:27 ` Dmitry A. Kazakov
2017-11-02 13:21 ` Simon Wright
2017-11-02 13:34 ` Dmitry A. Kazakov
2017-11-06 22:58 ` Robert A Duff
2017-11-07 11:50 ` Simon Wright
2017-11-17 0:51 ` Randy Brukardt
2017-11-17 8:32 ` Dmitry A. Kazakov
2017-11-18 1:14 ` Randy Brukardt
2017-11-18 9:19 ` Dmitry A. Kazakov
2017-11-20 5:40 ` J-P. Rosen
2017-11-20 8:22 ` Dmitry A. Kazakov
2017-11-20 22:03 ` Randy Brukardt
2017-11-21 10:26 ` Dmitry A. Kazakov
2017-11-22 0:56 ` Randy Brukardt
2017-11-22 1:14 ` Paul Rubin
2017-11-23 0:15 ` Randy Brukardt
2017-11-23 0:19 ` Victor Porton [this message]
2017-11-23 1:09 ` Paul Rubin
2017-11-28 0:24 ` Randy Brukardt
2017-11-22 8:42 ` Dmitry A. Kazakov
2017-11-23 0:19 ` Randy Brukardt
2017-11-23 1:11 ` Paul Rubin
2017-11-23 8:37 ` Dmitry A. Kazakov
2017-11-28 0:19 ` Randy Brukardt
2017-11-23 8:42 ` G. B.
2017-11-23 19:57 ` Blady
2017-11-23 21:30 ` J-P. Rosen
2017-11-23 23:24 ` Shark8
2017-11-23 22:13 ` Dennis Lee Bieber
2017-11-28 0:34 ` Randy Brukardt
2017-11-02 8:39 ` Stefan.Lucks
2017-11-02 10:29 ` Simon Wright
2017-11-02 10:37 ` Dmitry A. Kazakov
2017-11-02 16:54 ` Jeffrey R. Carter
2017-11-02 17:17 ` Simon Wright
2017-11-02 3:53 ` gautier_niouzes
2017-11-02 11:15 ` joakimds
2017-11-06 19:33 ` G. B.
2017-11-06 20:53 ` Pascal Obry
2017-11-06 21:07 ` Dmitry A. Kazakov
2017-11-06 21:14 ` Pascal Obry
2017-11-06 21:21 ` Dmitry A. Kazakov
2017-11-17 0:57 ` Randy Brukardt
2017-11-17 8:40 ` Dmitry A. Kazakov
2017-11-17 9:12 ` Simon Wright
2017-11-18 1:27 ` Randy Brukardt
2017-11-18 2:29 ` Dennis Lee Bieber
2017-11-18 9:32 ` Dmitry A. Kazakov
2017-11-06 21:16 ` Simon Wright
2017-11-06 21:43 ` Pascal Obry
2017-11-17 0:59 ` Randy Brukardt
2017-11-06 22:37 ` Robert A Duff
2017-11-07 2:25 ` Dennis Lee Bieber
2017-11-07 8:34 ` Dmitry A. Kazakov
2017-11-08 22:49 ` Robert A Duff
2017-11-09 8:49 ` Dmitry A. Kazakov
2017-11-09 15:36 ` AdaMagica
2017-11-09 16:58 ` Dmitry A. Kazakov
2017-11-09 18:10 ` AdaMagica
2017-11-09 20:05 ` Dmitry A. Kazakov
2017-11-09 21:11 ` AdaMagica
2017-11-09 21:38 ` Dmitry A. Kazakov
2017-11-09 22:52 ` AdaMagica
2017-11-10 8:18 ` Dmitry A. Kazakov
2017-11-10 18:21 ` J-P. Rosen
2017-11-10 19:34 ` Dmitry A. Kazakov
2017-11-11 11:32 ` AdaMagica
2017-11-11 12:17 ` Dmitry A. Kazakov
2017-11-11 15:38 ` AdaMagica
2017-11-11 21:36 ` Dmitry A. Kazakov
2017-11-12 5:21 ` J-P. Rosen
2017-11-14 16:49 ` Robert Eachus
2017-11-14 17:34 ` Jeffrey R. Carter
2017-11-17 1:11 ` Randy Brukardt
2017-11-17 8:42 ` Dmitry A. Kazakov
2017-11-10 20:30 ` G. B.
2017-11-17 1:08 ` Randy Brukardt
2017-11-09 22:43 ` Robert A Duff
2017-11-09 22:56 ` AdaMagica
2017-11-10 8:22 ` Dmitry A. Kazakov
2017-11-10 15:47 ` Robert A Duff
2017-11-10 15:54 ` Dmitry A. Kazakov
2017-11-14 15:58 ` Robert Eachus
2017-11-14 16:22 ` Dmitry A. Kazakov
2017-11-17 1:16 ` Randy Brukardt
2017-11-17 1:06 ` Randy Brukardt
2017-11-09 18:08 ` Simon Wright
2017-11-09 20:07 ` Dmitry A. Kazakov
2017-11-07 17:41 ` Jeffrey R. Carter
2017-11-08 10:20 ` Brian Drummond
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox