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
smime.p7s
Description: S/MIME cryptographic signature
____________________ Racket Users list: http://lists.racket-lang.org/users
