Lambda the Ultimate

From ICFP '06, the 1st informal Workshop on Mechanizing Metatheory comes Nick Benton's "Machine Obstructed Proof: How many months can it take to verify 30 assembly instructions?". It is a one page paper, but seems deserving of some notice.

Nick Benton offers a critique of Coq from the standpoint of an inexperienced user, although I am not sure I would really categorize Benton as "inexperienced". Some interesting quotes:

• "...I have rarely felt as stupid and frustrated as I did during my first few weeks using Coq."
• "Tactical theorem proving is like an extreme form of aspect-oriented programming. This is not A Good Thing...."
• "Just having intermediate stages of the work in a computerized form...proved a major benefit."
• "Automated proving is not just a slightly more fussy version of paper proving and neither...is it really like programming."
• "...but the payoff really came the second time I used Coq: I was able to prove some elementary but delicate results...in just a day or so."

[On edit: moved to a story from a forum post. Sorry. - TM]

While studying the conference program of the upcoming OOPSLA 2006 I discovered under the category "essay" an author who has quite something critical to say about AOP:

Aspect-oriented programming is discussed as a promising new technology. Like object-oriented programming, it is beginning to pervade all areas of software engineering. With its growing popularity, practitioners and academics alike are beginning to wonder whether they should start looking into or it, or otherwise risk having missed an important development. The author of this essay finds that much of aspect-oriented programming's success seems to be based on the conception that it improves both modularity and the structure of code, while in fact, it actually works against the primary purposes of the two, namely independent development and understandability of programs. Not seeing any way of fixing this situation, he thinks the success of aspect-oriented programming to be paradoxical.

This is not just another internet rant about the latest PL hype but the author, Friedrich Steimann, had done interesting work about AOP before. In particular his latest paper about typed AOP:

AOP and the antinomy of the liar

but also his award winning former critical AOP review:

Domain models are aspect free

The goal of my project was to be able to thoroughly test a poker server using poker bots. Each poker bot was to to excercise different parts of the server by talking the poker protocol consisting of 150+ binary messages. The poker server itself is written in C++ and runs on Windows....

This app is all about binary IO, thousands of threads/processes and easy serialization. All I ever wanted to do was send packets back and forth, analyze them and have thousands of poker bots running on my machine doing same. Lofty but simple goal :-). Little did I know!

Erlang and Haskell compared... Want to know the conclusion?

I was able to finish the Erlang version 10 times faster and with 1/2 the code. Even if I cut the 10-11 weeks spent on the Haskell version in half to account for the learning curve, I would still come out way ahead with Erlang.

I am sure you'll find a lot to disagree with in this article...

How I got here was, two recent pieces of writing that made me think heavily were Ruby-centric: Mikael Brockman’s Continuations on the Web and Sam Ruby’s Rails Confidence Builder... So I went and bought Programming Ruby ('Pickaxe' in the same sense that Programming Perl is the 'Camel book')

The conclusion of this piece is that Ruby looks like more than a fad, so LtU readers who still haven't checked it out might want to do so...

Where are the other editors, I wonder?

Ehud, theoretically on vacation, emailed me a link to an article from the June ACM Queue, Syntactic Heroin:

User-defined overloading is a syntactic drug that has seduced all too many language designers, programmers, and project managers.

It's focused on overloading in C++, and in particular the problems that can arise with implicit conversions, both built-in and programmer-defined. The author concludes that this is all a very bad idea, although to my disappointment, he doesn't explore more disciplined approaches to "overloading" in languages that are less conversion-happy, such as parameterized higher-order modules in functional languages, or Haskell's typeclasses.

The ever-enticing search for the ideal programming language produced this 1997 article from Sergey Polak. Although somewhat dated, I liked the article's comments about strings:

The discussion of arrays also brings to mind the subject of strings. No matter what anyone says, it is my firm belief that any language, regardless of its purpose, must have a powerful and flexible string-handling facility built-in. A program is very rare if it has no need for string handling, and I myself have had to write a great deal of programs, both at work and for my own uses, that depended heavily on strings. Some languages put strings in as an afterthought, and others put in some very basic features and leave the rest to library routines. That just can not be. The text string is a fundamentally important data type and can not be ignored, nor can it be relegated to blatant impersonation by some other type, such as array of characters. A string data type is required in a good language.

The very popular language C, and C++ as well, have horrendous string-handling facilities. Not only is the programmer required to declare his strings as character arrays, but there simply is no way to deal with strings as entities in the language.

Ouch. So true. That is not to endorse the specific string implementation recommendation from the article. (I have previously commented about implementation ideas, including communication buffers.)

Do the man a favor and save the article to disk for offline reading so as to minimize his bandwidth hits.

P.S. You're welcome, Ehud. I'll now be Internet-disabled for a week.