“Persistent” is older than I thought

“Persistent” usually refers to data that persists across multiple executions of a program. But in the last few years I've occasionally heard it used, especially in the Clojure community, for data structures that are updated nondestructively. (The old version persists after the update — get it?)

I saw this as a newfangled sloppy usage, but it ain't so. Like many seemingly new usages, it's surprisingly old. It dates back at least to 1985, when it appears prominently in Sarnak & Tarjan's Planar Point Location Using Persistent Search Trees. It was popularized a few years later by the same authors plus two others in Making Data Structures Persistent, and Tarjan has used it many times since then.

The more common sense — data that persists across program executions — is not much older. The earliest uses I've found are from several papers in 1976. Earlier ones are about either persistence of phosphors (an important issue for CRTs) or fault-tolerance by persistently retrying. It apparently caught on quickly, at least in the database community, because Jim Gray's 1977 Notes on Data Base Operating Systems takes it as standard enough to use without bothering to define it.

So it's reasonable to object to “persistent”=“nondestructive” because it conflicts with a more important concept, but not because it's new.

Maybe now someone will tell me it's in some very standard source like Knuth and I never noticed...

A sound bug finder is an unsound correctness prover

This account of Coverity, a commercial bug-finding tool for C and C++, illustrates a peculiar attitude common in the program-checking field:

we were also unsound. Our product did not verify the absence of errors but rather tried to find as many of them as possible. Unsoundness let us focus on handling the easiest cases first, scaling up as it proved useful. We could ignore code constructs that led to high rates of false-error messages (false positives) or analysis complexity, in the extreme skipping problematic code entirely (such as assembly statements, functions, or even entire files). Circa 2000, unsoundness was controversial in the research community, though it has since become almost a de facto tool bias for commercial products and many research projects.

Most program checkers prove theorems about programs. In particular, most aim to prove programs correct in some respect (e.g. type safety). A theorem prover is sound iff all the theorems it proves are true. So a correctness-prover that claims a buggy program is correct is unsound, but one that rejects a correct program is not. People in the program-checking field are accustomed to this, so they habitually think soundness = proving the absence of bugs.

But a bug-finder doesn't aim to prove correctness. Instead, it aims to prove incorrectness: to prove the presence of bugs. It's sound iff all the bugs it reports are real bugs — that is, if it has no false positives. False negatives (overlooking bugs) are OK, because they don't make its claims incorrect.

Unfortunately, most interesting properties are undecidable, so a checker can't be sound at both bug-finding and correctness-proving, unless its claims are very weak.

So Coverity did the right thing, in theory as well as practice, when they focused on suppressing false positives. Their bug finder was unsound, but it was unsound because it reported spurious errors, not because it missed some real bugs.

Addendum: bug finders in languages

The most visible bug finders (especially in academia) are those, like the ML typechecker, that try to prove something about the program, and report a bug if they fail. These are unsound as bug finders, since they sometimes report nonexistent bugs. Unfortunately, bug finding is their main use, so their standard of soundness does not fit.

This is particularly problematic for checkers that are built in to a compiler, and don't just complain but prevent programs from running. (This is part of why they're so visible — if the checker makes mistakes you can't ignore, you have to be aware of it.) It's hard (especially in theory) to justify a compiler that rejects correct programs. Sound bugfinders don't have this problem.

Why Lambda the Ultimate doesn't make me feel stupid

This search term appeared in my referer logs a few years ago: “lambda the ultimate makes me feel stupid”.

I used to feel that way — at least, I felt ignorant and despised. The denizens of LtU know an intimidating amount of theory, and some are quick to scorn anyone who doesn't, and demand that they read heaps of literature (often of dubious quality or relevance) before being permitted to talk. Not having read most of that literature, I accepted their evaluation, and felt ignorant.

But then battles of the War of Types erupted there, and λ the Ultimate became λT the Ultimate, or even System F the Ultimate. Anyone who dared suggest that dynamic typing was a reasonable basis for a language, or even a meaningful concept, faced voluminous condescension and condemnation. The seemingly knowledgeable scholars appeared to neither know nor care about the fundamental concepts of their field, and treated its greatest successes with learnèd disdain.

I do respect very much the elephant, and if your work dismisses him as an ill-formed dinosaur, it is not zoology.

(I don't think the dynamic typists gave a good account of themselves either; there was lots of handwaving about flexibility and little mention of the importance of simple semantics. But I found them less offensive, not only because I agree with them, but because they didn't demand the anathematization of the other side, nor of the object of study.)

The War of Types subsided, and LtU became once more a place of academic quiet, disturbed only by announcements of new PL papers. It still makes me feel ignorant at times, but it no longer makes me feel stupid. Sometimes it even makes me feel wise. Which is a much more dangerous emotion. When I feel stupid or ignorant, I study to become less so, but when I feel wise, I do nothing.

Exceptions are (mostly) for humans

Most languages have a way to signal a generic error with a string as the error message. This makes it easy to include relevant information in the description of the error: something as simple as (error "serve-ice-cream: quantity=~S must be positive" q) provides a human-readable description with whatever information you think is relevant. It's not machine-readable, but most errors don't need to be handled mechanically, so this is not usually a problem.

Languages with exception systems also allow signalling errors in a machine-recognizable way, typically by defining a new exception class. This is often considered the “proper” way to signal errors, but it's more work than a generic error, so it's typically done only for polished public interfaces. Errors that aren't exposed in such an interface (or aren't intended to be exposed — errors are a kind of implementation detail that's hard to hide) generally make do with strings.

When you do create an exception class, it's also more work to include relevant information in the exception. Typically you have to define slots, arrange for them to get the appropriate values, and then embed them in the error message. This requires changing several parts of the definition as well as the call site, so it's enough trouble that you often won't do it. Error reporting code is seldom high on the priority list until the error happens.

I ran into this problem a while ago, in a utility function which reported a rare error by throwing a C++ exception class like this:

class negative_error : public domain_error {
public:
    not_integer_exn() : domain_error("value must not be negative") {}
};

This was fine until the error finally happened. A high-level catch-almost-anything handler caught the exception and displayed the error message, which told me almost nothing about the problem. Since this was C++ and not running under a debugger, there was no automatic stack trace, and no hint of what value was negative, or who cared, or why. If I had been lazy and signaled the error with throw domain_error("serve_ice_cream: quantity=" + to_string(q) + " must not be negative"), the relevant information would have been in the string, but because I had done it the “right” way, it was not.

(The designers of C++ are aware of this problem. That's why all the standard exceptions take strings. negative_error should have too.)

In an ideal exception system, convenience and machine-readability would not conflict. It should be easy to signal an an-hoc error with a human-readable message and machine-recognizable fields. It might help to allow throwing exceptions without declaring them first, e.g. (throw '(negative-error domain-error) :quantity q "value must not be negative"). (Wasn't this allowed in some early exception systems?) But if it's only easy to have one of the two, choose the convenient human-readable form. That's the one you'll use.

What happened to “manifest” and “latent”?

Chris Strachey has remarkably influential lecture notes. His 1967 Fundamental Concepts in Programming Languages introduced or popularized a lot of now-standard terminology: r-value and l-value, first-class, polymorphism (ad-hoc and parametric), and maybe parametric type.

It also introduced some terms which didn't catch on, among them manifest and latent:

We call attributes which can be determined at compile time in this way manifest; attributes that can only be determined by running the program are known as latent.

These are the concepts now called “static” and “dynamic”. I'm not sure why Strachey bothered to introduce his own words for them, since the standard ones already existed, and he was evidently more comfortable with them — when he discusses types on the same page, he consistently uses “dynamic”, not “latent”. (Was “dynamic typing” already a standard term by 1967?) Maybe he reserved “static” and “dynamic” for behaviour, and wanted different words for the time when a property could be determined.

He acknowledges that the boundary between static and dynamic is fuzzy, and explains why it's useful anyway:

The distinction between manifest and latent properties is not very clear cut and depends to a certain extent on questions of taste. Do we, for example, take the value of 2 + 3 to be manifest or latent? There may well be a useful and precise definition—on the other hand there may not. In either case at present we are less interested in the demarkation problem than in properties which are clearly on one side or other of the boundary.

I wish more academics dared to do that.

Neither “manifest” nor “latent” caught on, and they might have been forgotten like most new coinages — but decades later, both have been resurrected with new meanings in connection with type. “Manifest typing” now refers to languages that require type declarations — an important concept that lacked a short name. “Manifest” is readily reinterpretable as “appearing in source”, and while it might confuse people who remember the old sense, we are few. Less usefully, “latent typing” serves as a euphemism for “dynamic typing” among type-theory partisans (bizarrely, as the word they object to is “type”, not “dynamic”, but at least it avoids using the terminology of the savages). In neither case does Strachey's original meaning survive; if you speak of some property other than type as “manifest” or “latent”, most proglang researchers will not understand.

Where do closures come from?

Common Lisp's function form is usually described as a device for switching between namespaces: it evaluates its argument in the “function” namespace instead of the normal “variable” namespace.

Older sources have a completely different idea: they say function makes closures. The Hyperspec says:

If name is a lambda expression, then a lexical closure is returned.

and

function creates a closure of the lambda expression

Both of these lines were inherited from CLtL, so this is not a new interpretation, nor one incompatible with the best of knowledge. What's going on?

To begin with, these two interpretations of function aren't observably different in portable Common Lisp. The only portable way to get a closure is by (function (lambda ...)) or by macros like defun that might expand to it. ((lambda ...) expands to (function (lambda ...)), because unlike all other special forms, lambda is in the function namespace, but that's just a historical quirk.) The only way to use lambda without function is ((lambda ...) ...), which has the same semantics regardless of whether it makes a closure. So portable code can't tell the difference.

Implementation-specific extensions can. If compile is extended to non-null lexical environments, it will make closures out of lambda-expressions without any help from function. Or if there's a named-lambda form that makes closures, it's unnecessarily complex to attribute the closure in (function (lambda ...)) to function.

So Common Lisp culture favors the simpler interpretation: lambda makes closures, and function is a mere namespacing operator.

Like so many oddities of CL, the old interpretation comes from Lisp Machine Lisp. The 1984 Lisp Machine Manual introduces function by saying it “has two distinct, though related, meanings.” The first is to get a symbol's function definition, and the second is to make a closure:

(let (a)
  (mapcar (function (lambda (x) (push x a))) l))
passes mapcar a specially designed closure made from the function represented by (lambda (x) (push x a)). When mapcar calls this closure, the lexical environment of the function form is put again into effect, and the a in (push x a) refers properly to the binding made by this let.

These two meanings were reflected in implementations. Guy Steele's reference interpreter (in the CL mailing list archive) doesn't bother to make a closure for ((lambda ...) ...), only for (function (lambda ...)). But when optimizing compilers became the norm, it no longer seemed silly (or inefficient) for lambda to always make a closure, so reinterpreting function as a namespacing operator made sense.

Surprisingly, this is not the first time function has been reinterpreted. The Pitmanual says Maclisp's function didn't make closures — it took a different form, *function, to even partially do that. function was equivalent to quote, except that in compiled code it would make a compiled function instead of just a lambda-expression — it permitted compilation but didn't change scoping. When Lisp Machine Lisp changed it to make closures, that was largely backward compatible, since most lambdas were intended to use lexical scope anyway. (I'm not sure when compilers started to use lexical scope — was that in Maclisp?)

I don't think any other language construct has had so many unrelated meanings over the years, let alone done so while preserving the meaning of existing code. function was originally a hint to the compiler, then a way to make closures, and then a namespacing operator. Its history probably ends there, since most new lisps eschew multiple namespaces and omit function rather than repurpose it, but three unrelated meanings is impressive.

Trivial program checkers

Typecheckers get (and deserve) a lot of attention for their ability to find bugs, but their success leads people to think typechecking is the only way to check programs. It's not. There are useful program checkers much simpler than any typechecker. Here's an example:

grep scanf

This finds real bugs in real programs — and not just ordinary bugs, but security holes due to %s overflowing buffers.

Here's another checker:

grep 'printf[^"]*$'

This finds printfs that don't have a literal string on the same line, which usually means someone forgot the format string and did this:

fprintf(file, somestr);

...instead of this:

fprintf(file, "%s", somestr);

It's a stupid bug, yes, but not a rare one. I once ran this checker on a large application and found dozens of instances of this bug. I also found dozens of false positives, from things like these:

snprintf(somewhere->buffer, MAX_BUFFER,
         "format string", args);
fprintf(file, message_format_strings[status], description);

But they were obvious false positives, so it was easy to ignore them.

Here's an even less selective checker:

grep '(\w\+ \?\*)'  #beware different versions of grep

This finds pointer typecasts, which (in C++, more than in C) are often misguided — they might indicate unsafe downcasts, or non-type-safe containers, or casting away constness, or simple unnecessary casting. It also finds a great many false positives, of course — mostly function prototypes and innocent casts.

These checkers don't prove the absence of the errors they look for. A program that doesn't contain the string scanf might still call it via a library or by dlsym. The printf checker can be defeated by something as simple as a printf-like function whose name doesn't contain printf — hardly a rare occurrence! The cast checker misses mundane things like (char**) and (IntPtr). They only find bugs; they don't guarantee their absence.

They're also not very powerful. They find only certain specific errors, not a wide variety. A real lint program can do much better.

But when you don't have a real lint handy, or when your lint doesn't find the problem you're worried about, simple textual checkers can be valuable.

“They only find bugs”. “Only certain specific errors”. Faint criticism.

In addition to being useful, these checkers are a reminder that there are many ways to check programs. None of them are typecheckers in either sense — not in the common sense, because they don't check datatypes, and not in the type-theory sense, because they don't classify expressions. They aren't even aware of the existence of expressions — they see code only as text. This is not a very powerful approach, but it's enough to find a lot of bugs.

Not all checkers are typecheckers.