FOM: Re: Re: Re: Godel, f.o.m.

[Andrej Bauer]

Steve Stevenson <steve at cs.clemson.edu> writes:

> Being an old compiler man, I know how little we understand about the
> language side. Theories about the pragmatics of programming
> languages are --- and should be --- formal but we don't use them
> much in real compiling. It is hard to reason without clear formal
> statements about what a language does *that is enforced and
> verifiable in any compiler for that language*. Until we can do that,
> my own feelings are that it is interesting but not usable.

It seems to me the future is closer than you think.

Here at CMU the compiler technology is the heaviest consumer of type
theory. The intermediate stages of compilation are supported by
"intermediate typed languages" that have formal models. So it's all
supported by lots of healthy math. The practice of formally specifying
a compiler is a research issue today. Let's give it ten years to
trickle into the "real world".

--
Andrej Bauer
http://andrej.com