# Re: Are there different programming languages that are compiled to the same intermediate language?

## arnold@freefriends.org (Aharon Robbins)

01 Feb 2023 08:07:24 GMT

*From comp.compilers*

Related articles |

Re: C arithmetic, was Software proofs, was Are there different *Keith.S.Thompson+u@gmail.com (Keith Thompson)* (2023-02-05) |

Re: C arithmetic, was Software proofs, was Are there different *gah4@u.washington.edu (gah4)* (2023-02-06) |

Re: C arithmetic, was Software proofs, was Are there different *DrDiettrich1@netscape.net (Hans-Peter Diettrich)* (2023-02-07) |

Re: C arithmetic, was Software proofs, was Are there different *gah4@u.washington.edu (gah4)* (2023-02-08) |

Re: C arithmetic, was Software proofs, was Are there different *anton@mips.complang.tuwien.ac.at* (2023-02-08) |

Re: C arithmetic, was Software proofs, was Are there different *DrDiettrich1@netscape.net (Hans-Peter Diettrich)* (2023-02-08) |

Re: C arithmetic, was Software proofs, was Are there different *gah4@u.washington.edu (gah4)* (2023-02-09) |

[6 later articles] |

| List of all articles for this month |

**From: ** | arnold@freefriends.org (Aharon Robbins) |

**Newsgroups: ** | comp.compilers |

**Date: ** | 01 Feb 2023 08:07:24 GMT |

**Organization: ** | non |

**References: ** | 23-01-092 |

**Injection-Info: ** | gal.iecc.com; posting-host="news.iecc.com:2001:470:1f07:1126:0:676f:7373:6970"; logging-data="7064"; mail-complaints-to="abuse@iecc.com" |

**Keywords: ** | translator, theory, comment |

**Posted-Date: ** | 01 Feb 2023 14:38:40 EST |

**Originator: ** | arnold@freefriends.org (Aharon Robbins) |

I've never understood this. Isn't there a chicken and egg problem?

How do we know that the theorem prover is correct and bug free?

I ask in all seriousness.

Thanks,

Arnold

In article 23-01-092, Martin Ward <martin@gkc.org.uk> wrote:

*>On 30/01/2023 10:00, John Levine wrote:*

*>> [Remember that while the halting problem is insoluble in general, it's*

*>> often soluble in specific cases, e.g. "halt" or "foo: goto foo".*

*>*

*>More usefully, there are methods for transforming a formal*

*>specification into an executable implementation which*

*>preserve semantic equivalence, and therefore are guaranteed*

*>to produce a terminating program (for input states for which*

*>the specification is defined). ...*

[It's a perfectly reasonable question. Alan Perlis, who was my thesis

advisor, never saw any reason to believe that a thousand line proof

was any more likely to be bug-free than a thousand line program.

-John]

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.