Re: Verified compilers?

[Brian Drummond <brian@shapes.demon.co.uk>]

On Sat, 10 Mar 2012 00:13:19 +0200, Niklas Holsti wrote:

> On 12-03-08 22:40 , Dmitry A. Kazakov wrote:

>> I didn't want to become a programmer, it just happened to me during 5th
>> or 6th semester. That time I was exposed to the classical Aho and
>> Ullmann.
> 
> That is the book we used. I don't remember the edition.

Heh - I remember poring over it in a bookstore - several times - and 
deciding I didn't like it. I can't remember exactly why, but it felt like 
formalism for formalism's sake, rather than as a tool to get anything 
done.

>> I was saved by David Gries. He is a really great man, who deserves all
>> possible fame and respect. His book on compiler construction opened my
>> eyes.

I thought Gries was better, but my own favourite was
"Understanding and Writing Compilers: A Do-it-Yourself Guide"
by Richard Bornat. 
Quite hard to find nowadays (though I think I found a PDF of it).
It does cover formal grammars - perhaps less fully, but clearly and from 
a practical aspect (i.e. assuming you would rather implement a parser 
than prove its grammar). 
But it covers other aspects - admittedly for older languages, but since 
it covers ALGOL (stack and heap), and SIMULA (closures) - all very much 
as a tool to get something done.

- Brian