Fastidious Elegance

(Open the image to view full size.)

Those who know me know that I like graphical text editors, as well as some not so graphical ones. When I am not hacking away in ed(1) or leveraging Unicode to its fullest potential, I am a big fan of the NEdit text editor, which I standby as one of the best text editors for UNIX today.

One of the great things about NEdit is how deceptively simple its powerful features are. Today I want to highlight its syntax highlighting, which is stupidly simple, but remarkably usable and powerful. Above, in the screen shot, you can see a simple looking window with a lot going on. The document is a CWEB program. WEB documents represent an interesting challenge to syntax highlighters, as they need to combine three different languages into a single, readable syntax. There is the documentation language, which, in this case, is TeX, and the programming language, which, in this case, is C. These are glued together by the CWEB meta language, which consists of a series of control codes to annotate code and prose. That's three languages, with three different syntaxes, all residing in the same file.

Many editors have simple, but less capable syntax highlighters, while others have very powerful syntax highlighting, but with very little in the way of easy configuration. This makes it difficult to create, say, a CWEB syntax highlighting format that works well in an hour or so. With the simpler syntax highlighting systems, you just could not do it. With the more complex systems, you can definitely do it, but it will take a bit longer than you might have expected or wanted to spend.

NEdit, on the other hand, allowed me to create the syntax highlighting that you see in the screenshot above in a matter of an hour or so, including the time it took to get the colors the way that I wanted them. [Note: if you are interested, the color scheme is Solarized, an overhyped color scheme that actually happens to look really good on my monitor and gives me just enough contrast to be happy.] Want more? What if I told you that I was able to create that syntax highlighting within NEdit's graphical syntax highlighting control, using nothing but some regular expressions and my mouse? Yes, that's right, I was able to get this highlighting with a very simple, common spec (regular expressions) and a graphical syntax highlighting tool built in to the editor. That's one of the great things about NEdit. The GUI interface is actually useful! Unlike many graphical editors, NEdit's GUI is practical, powerful, and productive, which is more than can be said for many other editors' so called GUI, which I usually disable.

I do not have space in this article to go through all of the other great features of NEdit, but I hope that this little view into syntax highlighting will allow you to appreciate the simple elegance of a well designed editor.

I usually use the Xterm terminal emulator when I am in mostly vanilla environments or in those cases when I do not want some of the other terminal emulators that one could choose. Xterm is a good, quiet workhorse that does its job well. There are a few things that I do not like about it, but otherwise, it's probably the terminal emulator on which I spend the majority of my time.

However, I have always found the default configuration of fonts with Xterm to be a real pain. They are always too small, and always setup with a color scheme (usually black on white) that just hurts my eyes when too many of them show up in a dimly lit room. Usually I go through a few incantations to get something close to reasonable out there, but until today, I have stuck with the bitmap infrastructure for fonts in Xterm. This means that I have lost out on modern advances in anti-aliasing that can make some of the nicer fonts really nice. Some other fonts just do not look good without anti-aliasing, whereas some really do not want to have you running anti-aliasing on them. Regardless, I always increase the font size of the default setup to match my monitor DPI, and I choose a better font than the default.

Today I finally took a look at the Xft facilities in Xterm, quite accidently. In there, I found that using only the renderFont and fontFace resources, I can get Xterm's fonts to look really great. That is because the renderFont resource controls whether or not Xterm takes advantage of Xft for font rendering. When it does take advantage of it, I get the good default scaling of fonts that actually takes into account how big my monitor DPI is. On the other hand, with fontFace, I can use a simpler font specification than the whole font-spec. For me, having done this so often, I do not get bothered by it much, because it really is not that hard to use the font-spec format, but for others this will come as a welcome way to avoid learning the font-spec format.

All in all, this simple pair of resources was all I needed to get my terminal fonts in order this time around. I am pleased with this.

Handwritten versions: Pg. 1, Pg. 2, Pg. 3.

Lately I have been playing with the Isabelle proof assistant, and I really like what I have been seeing. Isabelle has a lot of automation, and that is sort of one of my basic prerequisites when investigating proof systems. Isabelle has impressed me, though, because of how it has both automation and pretty great tools for creating well documented, readable theories.

In this essay I want to highlight one of these features: the Isar proof language. This really nice language allows a programmer to create clean, readable proofs, even elegant proof some of the time. In short, Isabelle's Isar language lets you write machine checkable proofs that read like paper proofs.

Lets consider a classic example of proving an iterative version of factorial is correct. The normal definitions and hand approach might look something like this:

f(n)    = 1          when n = 0
          n * f(n-1) otherwise

f'(n,t) = t           when n = 0
          f'(n-1,n*t) otherwise

Here we assume that the domains are over the natural numbers. Here is a simple proof by induction:

1. Assume n = 0, then f'(0,t) = t*f(0) by definition.
2. Assume f'(n,t) = t*f(n), then

    f'(n+1,t) = f'(n,(n+1)*t) by definition
             = (n+1)*t*f(n)  by induction hypothesis
             = t*f(n+1)      by definition and arithmetic

This proves f'(n,t)=t*f(n).

The above is about as simple an example as I can think of. Now, observe what this might look like when we do the same in an Isabelle theory; pay attention to the similarities and differences in the corresponding proofs.

primrec fact :: "nat => nat"
where "fact 0 = 1" | "fact (Suc n) = (Suc n) * fact n"

primrec fact_iter :: "nat => nat => nat"
where
  "fact_iter 0 t = t" |
  "fact_iter (Suc n) t = fact_iter n (Suc n * t)"

theorem fact_iter_correct: "fact_iter n t = t * fact n"
proof (induct n arbitrary: t)
  case 0 thus ?case by (simp add: fact_iter_def fact_def)
next
  case (Suc n) note hyp = this
  have "fact_iter (Suc n) t = fact_iter n (Suc n * t)" 
    by (simp add: fact_iter_def)
  also have "... = (Suc n * t) * fact n" 
    using hyp.
  also have "... = t * fact (Suc n)" 
    by (simp add: add_mult_distrib add_mult_distrib2)
  finally show ?case.
qed

Overall, I must say that this is the most readable proof I have seen in a system offering as much automation as Isabelle does. Also note that it is only slightly more verbose.

Handwritten versions: Page 1.

With all the dynamic and interactive interfaces we have for programming today, I want to mention something of a fault in the way that most people use things like REPLs and other interactive programming sessions. Viz., we usually throw all that scratch work away! Often, what we put in our interactive sessions is really the making of some valuable long term artifact.

One of the things I like about programming on paper is the automatic transcript of ideas and code that I can use later. Perhaps it becomes a new test case, or maybe a new section on simpler but erroneous versions of the function I am writing.

Fortunately, the interactive sessions I have used all support some type of transcript mechanism for saving work. So there really is no excuse: don't throw away all that work!

Handwritten versions: Page 1; Page 2.

The keyboard is the favored tool of the programmer. And why not? As an input device the keyboard has served us very well. I am pretty fast on a keyboard as a means of entering data. However, is the keyboard a good editing device? I have doubted this for some time now. In particular, I doubt whether a keyboard is the best means by which to accomplish many text editing tasks.

I am not suggesting that all editing tasks are better done with a mouse, just that some common tasks are completed more efficiently using mice or touchscreens. I would group these tasks under the umbrella of “Selection and Navigation.”

I consider use of arrow keys, Emacs' f, b, p, and n movement paradigm, and other keyboard shortcuts designed to move the insertion point set distances, to be misguided and inefficient.

Put simply, the mental overhead and time lost on sub-optimal combinations of keystrokes means that too much time overall is lost to keyboard navigation to make it worthwhile. Pointing devices just win if you need to quickly move or select blocks of text.

My evidence is video games. You find plenty of keyboard use in games, but when it comes to arbitrary selection and navigation, you find the mouse, and not the keyboard sitting comfortably on the throne.

I am not suggesting that programmers give up their favorite text editor, but I am suggesting that text editors spend more effort on providing a streamlined mousing experience in the same way that editors like Acme and Sam of Plan 9 fame make the mouse an integrated part of the editor, and not just an additional afterthought.