Lambda the Ultimate

The Sixth IBM Programming Languages Day will be held at the IBM Thomas J. Watson Research Center on Friday, April 22, 2005. The day will be held in cooperation with the New Jersey and New England Programming Languages and Systems Seminars. The main goal of the event is to increase awareness of each other's work, and to encourage interaction and collaboration.

Simon Peyton Jones is keynoting on composable memory transactions.

The program, and abstracts, are available online.

A computer-assisted proof of a 150-year-old mathematical conjecture can at last be checked by human mathematicians... ...Georges Gonthier, at Microsoft's research laboratory in Cambridge, UK, and Benjamin Werner at INRIA in France have proven the [Four Colour Theorem] in a way that should remove such concerns.

They translated the proof into a language used to represent logical propositions - called Coq - and created logic-checking software to confirm that the steps put forward in the proof make sense.

Georges Gonthier's home page includes links to the paper and the actual proof.

A very short paper having pretty narrow applicability, but somehow it is exactly what I needed today for my programming. Go figure.

The concept of a propositional logic, PL, will be defined and a method, to be referred to as the Kleene Search Procedure, will be used to determine the validity of formulas of PL. This method utilizes a set of sequent rules which are derived in a purely mechanical fashion from the truth tables which are the intended interpretations of the connectives of PL. The results are then used to show how a formal system, GPL, which is a sequent calculus can be constructed with very simple axioms and these sequent rules to yield the valid formulas of PL

Note that there are two "mechanical" algorithms here - one deriving sequent rules from truth tables, and another deriving either a proof ar a refutation of a sequent.

I wonder just how deeply this is related to both Qi and the map coloring theorem proof (didn't read any of those threads carefully yet).

Over at comp.lang.c++.moderated, there is a thread created by the c++ guru Scott Meyers on the subject: "Why do you program in c++?".

In my experience, C++ is alive and well -- thriving, even. This surprises
many people. It is not uncommon for me to be asked, essentially, why
somebody would choose to program in C++ instead of in a simpler language
with more extensive "standard" library support, e.g., Java or C#.

It's a truly neutral question: given that there are many
languages to choose from, why do you choose to program in C++? I don't
care if the reaons are technical, political, social, or what, I'm just
honestly curious.

I thought this might be interesting.