[racket] Aging code -- Algol 68

What is a type=theoretical program verifier? How does it related to modern things such as Coq/HOL/friends? 


On Jul 10, 2013, at 8:26 PM, Hendrik Boom wrote:

> How can I resist this request to talk about ancient code?  Even if it 
> seems off-topic?
> 
> My own long-lived examples are a type-theoretical program verifier, 
> and an Algol 68 compiler.
> 
> In 1972 I started an Algol 68 conpiler, worked on it for a few years at 
> the University of Alberta, decided to abandon the project when it went 
> over two and a half years (I had planned ono two) and my PDF expired, 
> went on to work at the Mathematical Centre in Amsterdam , where 
> against my better judgement I was persuaded to resue work on it.  The 
> facilities there were much worse than the ones I had had in Alberta.
> 
> When that time came to a close I had a compier that handles about half 
> of a very demanding test suite.
> 
> But that meant it was probably about 90% complete, but you really  
> needed closer to 99% to make the thing useful.
> 
> I backed it up on magnetic tape, left one copy in a friend's sock 
> drawer and took teh other with me.
> 
> Over the years the one I had got copied a few times, because 
> reel-to-reel 9-track tape drives were getting scarce.
> 
> Unfortunately, one time that copy was not done correctly, although it 
> appeared to have been done correctly.
> 
> Then a few years ago I found that someone on the other side of the 
> world had written an Algol W compiler (the language in which I had 
> written my compiler), and I tried to use it to resurrect my Algol 68 
> compiler.  When I discovered the bit rot I felt sick.
> 
> But my friend in Amsterdm had contacts within IBM, and someone there 
> took it on as a personal project.  It turned out he was working on 
> long-term data archiving, and he thought it was just *great* that he 
> gos a 30-year-old magnetic tape to try to recover data from.  For all I 
> know that tape might have been mentioned in some archiving conference 
> proceedings.
> 
> Anyway, I got the enntire compiler and a bunch of other data sent to me 
> in 8-bit EBCDIC code and proceeded to decode it.
> 
> I ended up with the source code to the compiler.  It was really fun to 
> be looking through it again.
> 
> Most of hte deficiencies I find looking at it are caused by
>  (1) It wasn't finished
>  (2) the limitations of Algol W.  Algol W was a pretty good tool for the 
> time, with garbage collection and data structures, but its limitations
> were severe.  No decent modern modules and separate compilation 
> mechanisms (although procedures could be separately compiled if they 
> didnt need any global variables) and limita on the size of procedures, 
> on the number of blocks in a compilation, and on the number of 
> different record types that could be used in a complete program (16 of 
> them).  There limitations rather warped the program from its  original 
> design.
>  I'd love to do the whole thing over, except that it might take a few 
> more years, and I don't think anyone would be interested in the 
> resultt.
> 
>  Nevertheless, I go back to work on it every now and then in 
> one-or-two-month spurts of energy.  Doingg this is kind of like playing 
> a video game of extreme complexity.  Each new test case passed is line 
> beating a boss.
> 
> A lot of code in the code generator got tossed or commented out, 
> because that class of machine just isn't around any more.  But I do 
> keep the old commented-out code around until I'm ready to ocmmit to the 
> new.
> 
> If anyone is interested in looking at the code, it's available from 
> the monotone repository at http://mtn-host.prjek.net/.  The algol W 
> compiler in that repository has bugs; it's *not* the version I'm 
> using, and I'm currently wondering how it's related to the one I *am* 
> using.
> 
> Every now and then I wake up in the middle of the night having 
> figured out once again how I should have approached the whole 
> project.
> 
> They vary a lot in detail, but the common threads are:
> 
> (1) I should have started with a simplified, significantly unoptimizing 
> code generator, then wrote test cases for it.
> 
> (2) I should have also started implementing a sublanguage -- a  
> sublanguage that contained only the features I really needed for 
> writing the compiler.
> 
> Actually, it wouldn't really have been a sublanguage -- it would have 
> had a subset of the semantics, but drastically simplified syntax, and 
> almost no implicit type conversions.  Kind of a compromise betwen a 
> programming language and a test generator for the code generator.
> 
> (3) write the real compiler in the sublanguage, extending the 
> sublanguage whenever implementing a feature was faster than coding 
> around its absence.
> 
> The history of the verifier is a tale for another day.
> 
> -- hendrik
> 
> ____________________
>  Racket Users list:
>  http://lists.racket-lang.org/users

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4373 bytes
Desc: not available
URL: <http://lists.racket-lang.org/users/archive/attachments/20130711/efaccf26/attachment.p7s>