From: antispam@math.uni.wroc.pl
Subject: Re: State of the compiler market
Date: Sun, 26 Feb 2017 17:35:29 +0000 (UTC)
Date: 2017-02-26T17:35:29+00:00 [thread overview]
Message-ID: <o8v3l1$3go$1@z-news.wcss.wroc.pl> (raw)
In-Reply-To: 87varxjouh.fsf@nightsong.com
Paul Rubin <no.email@nospam.invalid> wrote:
>
> I'm a FOSS supporter myself, but in the case of an alternate Ada
> implementation, I'd think the most interesting possibility would be for
> someone (maybe Adacore) to team up with the CompCert guys and make a
> verified Ada compiler.
Maybe a blasphemy here, but if you go trough full formal
verification does Ada offer significant advantages over C or
C++? L4.sec guys deliver code via C and apparently this did
not hamper their efforts. Potentially Ada may be more
productive, however in formaly verified project actual C coding
is likely to be small part of total effort, so replacing
C with Ada should not make much difference. I would think
that Ada strength is in intermediate area where better
checking in compiler and safer programming practices
lead to faster delivery of reasonably good program.
--
Waldek Hebisch
next prev parent reply other threads:[~2017-02-26 17:35 UTC|newest]
Thread overview: 82+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-02-23 0:26 State of the compiler market john
2017-02-23 3:17 ` Luke A. Guest
2017-02-23 5:16 ` Per Sandberg
2017-02-23 6:01 ` gautier_niouzes
2017-02-23 9:01 ` joakimds
2017-02-23 18:03 ` Jeffrey R. Carter
2017-02-24 9:23 ` Per Sandberg
2017-02-24 9:32 ` Paul Rubin
2017-02-23 21:22 ` Randy Brukardt
2017-02-24 16:36 ` john
2017-02-25 10:48 ` Ingo M.
2017-02-25 11:07 ` Jeffrey R. Carter
2017-02-25 14:25 ` Ingo M.
2017-02-25 17:30 ` Jeffrey R. Carter
2017-02-25 11:29 ` Dmitry A. Kazakov
2017-02-25 13:46 ` G.B.
2017-02-25 14:46 ` Ingo M.
2017-02-25 15:21 ` Dmitry A. Kazakov
2017-02-25 15:49 ` Ingo M.
2017-02-25 16:11 ` Dmitry A. Kazakov
2017-02-25 19:03 ` G.B.
2017-02-26 0:11 ` Luke A. Guest
2017-02-26 8:44 ` Dmitry A. Kazakov
2017-02-26 0:20 ` Luke A. Guest
2017-02-26 2:26 ` Randy Brukardt
2017-02-26 9:14 ` Paul Rubin
2017-02-26 17:35 ` antispam [this message]
2017-02-26 22:32 ` Paul Rubin
2017-02-27 2:38 ` antispam
2017-02-27 2:54 ` Paul Rubin
2017-02-27 3:54 ` antispam
2017-02-28 20:51 ` Randy Brukardt
2017-02-28 21:29 ` Luke A. Guest
2017-03-01 8:43 ` reinkor
2017-03-01 14:20 ` Adacore and licensing (again), was: " Simon Clubley
2017-03-01 17:02 ` reinert
2017-03-01 18:34 ` Simon Clubley
2017-03-05 19:38 ` Robert Eachus
2017-03-05 23:17 ` Luke A. Guest
2017-03-06 1:12 ` Dennis Lee Bieber
2017-03-06 2:56 ` Robert Eachus
2017-03-07 20:47 ` Simon Clubley
2017-03-08 0:23 ` Lucretia
2017-03-08 10:26 ` Simon Wright
2017-03-01 14:28 ` volkert
2017-03-01 15:01 ` J-P. Rosen
2017-03-01 16:05 ` G.B.
2017-03-06 23:15 ` john
2017-03-07 16:42 ` Dennis Lee Bieber
2017-06-27 8:29 ` Jacob Sparre Andersen
2017-06-28 10:40 ` Lucretia
2017-06-28 11:44 ` Dmitry A. Kazakov
2017-06-28 13:54 ` Luke A. Guest
2017-06-28 14:16 ` Dmitry A. Kazakov
2017-06-29 1:26 ` Shark8
2017-06-29 5:46 ` gautier_niouzes
2017-06-29 11:36 ` Lucretia
2017-06-29 12:23 ` gautier_niouzes
2017-06-29 12:50 ` Dmitry A. Kazakov
2017-06-29 14:47 ` Lucretia
2017-06-29 17:23 ` G.B.
2017-06-29 18:27 ` Jacob Sparre Andersen
2017-06-29 19:04 ` Lucretia
2017-06-29 19:01 ` Lucretia
2017-06-30 5:27 ` J-P. Rosen
2017-06-30 7:18 ` Dmitry A. Kazakov
2017-06-30 7:34 ` J-P. Rosen
2017-06-30 8:10 ` Dmitry A. Kazakov
2017-06-30 10:10 ` J-P. Rosen
2017-06-30 10:53 ` Dmitry A. Kazakov
2017-06-30 7:51 ` Jacob Sparre Andersen
2017-06-30 8:20 ` Dmitry A. Kazakov
2017-06-30 11:11 ` Lucretia
2017-06-30 11:23 ` Lucretia
2017-06-29 12:57 ` Petter Fryklund
2017-06-30 13:57 ` Alejandro R. Mosteo
2017-06-30 14:19 ` Lucretia
2017-07-01 8:06 ` darkestkhan
2017-07-01 9:17 ` Dmitry A. Kazakov
2017-02-26 10:14 ` Dirk Craeynest
2017-02-27 9:56 ` Ivan Levashev
2017-06-27 8:00 ` Jacob Sparre Andersen
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox