Re: Verified compilers?

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

On 14.03.12 09:36, Niklas Holsti wrote:
> On 12-03-12 11:43 , Dmitry A. Kazakov wrote:

>> No computer can parse infinite language
>> or compute incomputable. If you want to handle such stuff [and you must all
>> the time!] you have to map it onto some finite/computable framework and
>> deal within the latter.
>
> Exactly. But since our present computers can deal with very large numbers and programs indeed, the mathematical and technical methods we use for handling programming languages and programs cannot depend on this finiteness, but must use methods that apply to numbers and programs of unbounded size, but still of constrained form. Grammars are good for that, IMO.

Side note: WRT finiteness, language designers have made one
particular mistake again and again, following a convention,
by telling programmers about some type called REAL. The set
of supposed real numbers that programmers have heard about
before, in math lessons, is not finite---though no one has
ever seen it, giving rise to the question of a possible
misunderstanding of infinity. The values of reals include
numbers that are not rational, not a ratio, or fraction,
that is.

What the language designers usually mean, though, is some finite
Fraction_with_Split_Shifting thing, having infinitesimally
little to do with the reals. Consequence: an infinite supply
of surprises, cause by the name REAL.