public inbox for gcc@gcc.gnu.org
 help / color / mirror / Atom feed
From: Gabriel Dos Reis <gdr@integrable-solutions.net>
To: Georg Bauhaus <bauhaus@futureapps.de>
Cc: gcc mailing list <gcc@gcc.gnu.org>
Subject: Re: signed is undefined and has been since 1992 (in GCC)
Date: Tue, 28 Jun 2005 23:53:00 -0000	[thread overview]
Message-ID: <m3zmtakpig.fsf@uniton.integrable-solutions.net> (raw)
In-Reply-To: <42C1D610.6030701@futureapps.de>

Georg Bauhaus <bauhaus@futureapps.de> writes:

| Gabriel Dos Reis wrote:
| > Robert Dewar <dewar@adacore.com> writes:
| > | Gabriel Dos Reis wrote:
| > | | But the whole idea of hardware semantics is bogus, since you are
| > | assuming some connection between C and the hardware which does not
| > | exist. C is not an assembly language.
| > If you live in a different world, you may not see the connection.
| 
| I'm not sure whether this isn't just C's self-fulfilling
| prophecy at work: Many C programmers think that C is a high level

self-fulfilling prophecy or not, would you deny that processor
specific ABIs are published and programmers expect compilers to follow
them?  GCC itself relies on such connection.

| assembly language (at least in my real world).
| They start using C as if it were...

Well, I would not say it is something unique to C programmers.
Recently we had a guest working on compiler verification and model
checking, deeply rooted in the ML community explain us the
architecture of their proof checker.  The heart of the proof checker,
the trusted part, is written in C instead of SML.  When the question
was asked as to why -- probably because people were surprised, given their
close tie to SML -- and the answer was simple:  even though it can be
claimed that the C type system is unsound and SML's is sound, C is
trustworthy (and preferred over SML for that curcial part of the proof
checker) because the mapping of the C code to the generated assembly
code is straighforward and amenable to inspection.

-- Gaby

  reply	other threads:[~2005-06-28 23:53 UTC|newest]

Thread overview: 119+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2005-06-28  4:08 Andrew Pinski
2005-06-28  4:20 ` Michael Veksler
2005-06-28  9:49   ` Robert Dewar
2005-06-28  4:34 ` Gabriel Dos Reis
2005-06-28  4:50   ` Andrew Pinski
2005-06-28  5:13     ` Gabriel Dos Reis
2005-06-28  5:34       ` Andrew Pinski
2005-06-28  6:01         ` Gabriel Dos Reis
2005-06-28  9:18           ` Robert Dewar
2005-06-28 11:50             ` Gabriel Dos Reis
2005-06-28 12:07               ` Robert Dewar
2005-06-28 12:33                 ` Gabriel Dos Reis
2005-06-28 12:57                   ` Robert Dewar
2005-06-28 13:19                     ` Gabriel Dos Reis
2005-06-28 22:58                       ` Georg Bauhaus
2005-06-28 23:53                         ` Gabriel Dos Reis [this message]
2005-06-29  0:27                           ` Robert Dewar
2005-06-29  0:43                             ` Gabriel Dos Reis
2005-06-29  0:48                               ` Robert Dewar
2005-06-29  1:14                                 ` Gabriel Dos Reis
2005-06-29  1:21                                   ` Diego Novillo
2005-06-29  2:19                                     ` Marcin Dalecki
2005-06-29  3:13                                       ` Scott Robert Ladd
2005-06-28 14:24                     ` Olivier Galibert
2005-06-28 14:28                       ` Jonathan Wilson
2005-06-28 14:42                         ` Olivier Galibert
2005-06-28 14:39                       ` Dave Korn
2005-06-28 14:52                         ` Olivier Galibert
2005-06-28 15:01                           ` Robert Dewar
2005-06-28 15:04                           ` Andrew Haley
2005-06-28 17:18                             ` Olivier Galibert
2005-06-28 17:36                               ` Dave Korn
2005-06-28 18:02                                 ` Olivier Galibert
2005-06-28 18:36                                   ` Dave Korn
2005-06-28 18:56                                     ` Gabriel Dos Reis
2005-06-28 19:10                                     ` Olivier Galibert
2005-06-28 19:13                                       ` Andrew Pinski
2005-06-28 19:20                                         ` Robert Dewar
2005-06-28 21:48                                           ` Joe Buck
2005-06-28 19:25                                         ` Gabriel Dos Reis
2005-06-28 19:32                                           ` Robert Dewar
2005-06-28 19:48                                             ` Gabriel Dos Reis
2005-06-28 20:37                                               ` Robert Dewar
2005-06-28 20:58                                                 ` Gabriel Dos Reis
2005-06-28 21:57                                                   ` Robert Dewar
2005-06-28 21:44                                             ` Joe Buck
2005-06-28 21:50                                               ` Olivier Galibert
2005-06-28 21:59                                               ` Robert Dewar
2005-06-28 18:52                                   ` Robert Dewar
2005-06-28 19:17                                     ` Olivier Galibert
2005-06-28 19:21                                       ` Robert Dewar
2005-06-28 20:18                                         ` Paul Koning
2005-06-28 20:24                                           ` Robert Dewar
2005-06-28 21:41                                             ` Joe Buck
2005-06-28 21:53                                         ` Michael Veksler
2005-06-28 23:05                                           ` Michael Veksler
2005-07-02 17:15                                         ` Florian Weimer
2005-07-02 18:59                                           ` Gabriel Dos Reis
2005-07-02 23:20                                             ` Robert Dewar
2005-07-03  0:07                                               ` Gabriel Dos Reis
2005-07-03  9:49                                                 ` Robert Dewar
2005-07-02 23:12                                           ` Nicholas Nethercote
2005-07-02 23:20                                           ` Robert Dewar
2005-07-03  0:13                                             ` Gabriel Dos Reis
2005-07-03  9:54                                               ` Robert Dewar
2005-07-03 10:02                                                 ` Florian Weimer
2005-07-03 10:10                                                   ` Robert Dewar
2005-07-03 12:01                                                 ` Gabriel Dos Reis
2005-07-14  7:21                                           ` Marc Espie
2005-07-02 17:06                                 ` Florian Weimer
2005-06-28 17:51                               ` Joe Buck
2005-06-28 18:21                                 ` Gabriel Dos Reis
2005-06-28 18:53                                   ` Robert Dewar
2005-06-28 18:28                                 ` Olivier Galibert
2005-06-28 18:38                                   ` Dave Korn
2005-06-28 18:50                               ` Robert Dewar
2005-06-28 19:02                                 ` Gabriel Dos Reis
2005-06-28 19:17                                   ` Robert Dewar
2005-06-28 19:43                                     ` Gabriel Dos Reis
2005-06-28 20:31                                       ` Robert Dewar
2005-06-28 20:51                                         ` Gabriel Dos Reis
2005-06-28 20:59                                           ` Robert Dewar
2005-06-28 21:20                                             ` Gabriel Dos Reis
2005-06-28 21:27                                               ` Paul Koning
2005-06-28 21:39                                                 ` Andreas Schwab
2005-06-28 21:35                                               ` Joe Buck
2005-06-28 22:09                                     ` Joseph S. Myers
2005-06-28 22:16                                       ` Falk Hueffner
2005-06-29  6:59                                         ` Eric Botcazou
2005-06-28 22:19                                       ` Robert Dewar
2005-06-28 16:42                         ` Joe Buck
2005-06-28 17:10                           ` Dave Korn
2005-06-28 17:21                             ` Joe Buck
2005-06-28 22:41                               ` Georg Bauhaus
2005-06-28 14:47                       ` Gabriel Dos Reis
2005-06-28 16:38                     ` Joe Buck
2005-06-28 21:59                     ` Mike Stump
2005-06-28 13:47                   ` Gabriel Paubert
2005-06-28 13:52                     ` Andrew Pinski
2005-06-28 14:33                     ` Robert Dewar
2005-06-28 12:08               ` Robert Dewar
2005-06-28 12:34                 ` Gabriel Dos Reis
2005-06-28  7:25         ` Michael Veksler
2005-06-28 16:32           ` Joe Buck
2005-06-28 16:56             ` Joe Buck
2005-06-28 17:03             ` Gabriel Dos Reis
2005-06-28 17:34               ` Joe Buck
2005-06-28 18:09                 ` Gabriel Dos Reis
2005-06-28 17:35               ` Diego Novillo
2005-06-28  6:55       ` Steven Bosscher
2005-06-28  7:20         ` Michael Veksler
2005-06-28  7:39           ` Falk Hueffner
2005-06-28 12:08             ` Gabriel Dos Reis
2005-06-28 12:01         ` Gabriel Dos Reis
2005-06-28 16:59 Morten Welinder
2005-06-28 17:23 ` Olivier Galibert
2005-06-28 18:44 ` Michael Veksler
2005-06-28 17:41 Paul Schlie
     [not found] <2382433.1119938227627.JavaMail.root@dtm1eusosrv72.dtm.ops.eu.uu.net>
2005-06-28 19:44 ` Toon Moene

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=m3zmtakpig.fsf@uniton.integrable-solutions.net \
    --to=gdr@integrable-solutions.net \
    --cc=bauhaus@futureapps.de \
    --cc=gcc@gcc.gnu.org \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).