From: Mehdi Saada <00120260a@gmail.com>
Subject: Re: questions on input/output
Date: Sun, 7 Feb 2021 00:52:22 -0800 (PST) [thread overview]
Message-ID: <44f51d9b-2eaa-4073-b6b7-c3bced114697n@googlegroups.com> (raw)
In-Reply-To: <87pn1dlz84.fsf@nightsong.com>
Le samedi 6 février 2021 à 20:26:21 UTC, Paul Rubin a écrit :
> I don't know. To a pure beginner, probably not, but I wouldn't have
> suggested Ada either.
What is this heresy ?! Personally I never had an issue with the rigor, as a beginner I'm pretty happy the compiler is fø©kîng with my life constantly ;-)
> SPARK isn't that connected to proof theory--it's just a program that
> verifies contracts on Ada functions.
Of course but it makes no sense if you're not going to investigate proof making using these, so it is connected... in practice.
next prev parent reply other threads:[~2021-02-07 8:52 UTC|newest]
Thread overview: 18+ messages / expand[flat|nested] mbox.gz Atom feed top
2021-02-05 22:50 questions on input/output Mehdi Saada
2021-02-05 23:36 ` Jeffrey R. Carter
2021-02-06 0:59 ` Mehdi Saada
2021-02-06 1:34 ` Mehdi Saada
2021-02-06 2:13 ` Paul Rubin
2021-02-06 7:21 ` J-P. Rosen
2021-02-06 9:36 ` Dmitry A. Kazakov
2021-02-06 10:38 ` AdaMagica
2021-02-06 11:37 ` Mehdi Saada
2021-02-06 11:51 ` Mehdi Saada
2021-02-06 18:10 ` Paul Rubin
2021-02-06 18:55 ` Mehdi Saada
2021-02-06 20:26 ` Paul Rubin
2021-02-07 8:52 ` Mehdi Saada [this message]
2021-02-07 20:38 ` Paul Rubin
2021-02-07 9:55 ` Gautier write-only address
2021-02-07 22:54 ` Mehdi Saada
2021-02-06 11:47 ` Dmitry A. Kazakov
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox