Lambda the Ultimate

James H. Fetzer's Program Verification: The Very Idea (1988) is one of the two most frequently cited position papers on the subject of program verification. The other one is Social Processes and Proofs by De Millo, Lipton, and Perlis (1979), previously discussed on LtU. Fetzer's paper generated a lot of heated discussion, both in the subsequent issues of CACM and on Usenet.

It's not clear to me what all the fuss is about. Fetzer's main thesis seems pretty uncontroversial:

The notion of program verification appears to trade upon an equivocation. Algorithms, as logical structures, are appropriate subjects for deductive verification. Programs, as causal models of those structures, are not. The success of program verification as a generally applicable and completely reliable method for guaranteeing program performance is not even a theoretical possibility.

(See also part I, part II, and part III.)

Conrad Barski has posted a sneak peak from his upcoming Lisp textbook/comic: Land of Lisp.

The first slides may seem unrelated, but boy does the message sting when you reach the ending...

FPers will be quick to note, of course, that this being April Fools' Day the whole thing is a joke and we can all go back to Haskell...

It is argued that formal verifications of programs, no matter how obtained, will not play the same key role in the development of computer science and software engineering as proofs do in mathematics. Furthermore, the absence of continuity, the inevitability of change, and the complexity of specification of significantly many real progarms make the formal verification process difficult to justify and manage. It is felt that ease of formal verification should not dominate program language deisgn.

Niklaus Wirth. Good Ideas, Through the Looking Glass, IEEE Computer, Jan. 2006, pp. 56-68.

An entire potpourri of ideas is listed from the past decades of Computer Science and Computer Technology. Widely acclaimed at their time, many have lost in splendor and brilliance under today’s critical scrutiny. We try to find reasons. Some of the ideas are almost forgotten. But we believe that they are worth recalling, not the least because one must try to learn from the past, be it for the sake of progress, intellectual stimulation, or fun.

A personal look at some ideas, mostly from the field of programming languages. Some of Wirth's objections are amusing, some infuriating - and some I agree with...

LtU readers will obviously go directly to sections 4 (Programming Language Features) and 6 (Programming Paradigms). Here are a few choice quotes:

It has become fashionable to regard notation as a secondary issue depending purely on personal taste. This may partly be true; yet the choice of notation should not be considered an arbitrary matter. It has consequences, and it reveals the character of a language. [Wirth goes on to discuss = vs. == in C...]

Enough has been said and written about this non-feature [goto] to convince almost everyone that it is a primary example of a bad idea. The designer of Pascal retained the goto statement (as well as the if statement without closing end symbol). Apparently he lacked the courage to break with convention and made wrong concessions to traditionalists. But that was in 1968. By now, almost everybody has understood the problem, but apparently not the designers of the latest commercial programming languages, such as C#.

The concept that languages serve to communicate between humans had been completely blended out, as apparently everyone could now define his own language on the fly. The high hopes, however, were soon damped by the difficulties encountered when trying to specify, what these private constructions should mean. As a consequence, the intreaguing idea of extensible languages faded away rather quickly.

LtU readers are also going to "enjoy" what Wirth has to say about functional programming...

(Thanks Tristram)

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.