Writing Solid Code

After 10 short years as a university-level CS instructor, I’ve finally figured out the course I was born to teach. It’s called “Writing Solid Code” and covers the following topics:

  • Testing—There are lots of books on software testing but few that emphasize the thing I need students to learn, which is simply how to break code with minimum effort. There’s no book at all that covers fuzzing in a useful way (though Alex plans to write it). Lessons Learned in Software Testing is one of the better books I know of.
  • Debugging—I covered my view of debugging here a while ago and also plan to borrow material from nice books by Zeller, Agans, Butcher, and Metzger.
  • Assertions—I try to not be too dogmatic about stuff but CODE HAS TO HAVE ASSERTIONS. That is all there is to it. I’m in the middle of a long post about this and hope to publish it sometime in November.
  • Medium-weight formal methods—Probably using Frama-C to statically verify that assertions hold and language rules (array bounds etc.) are not violated on any path through the code.
  • Code reviews—I’ve been reading Wiegers but realistically I think the main thing is just to do a lot of code reviews.

Ideally this course would not be needed. Rather, the material would be implicit in the contents of lots of other courses and students would naturally acquire strong skills in defensive programming, testing, debugging, and code reviews. We do not appear to be doing a very good job of encouraging these skills to develop. Rather, we’re giving the students a four-year sequence of little fire-and-forget programming assignments with zero focus on code quality and where the code is thrown away after the due date. I believe this is doing them a disservice.

In my embedded software class this fall I’ve been trying a different approach where the students are working in groups and testing their own, and each others’, code in multiple rounds, and we’re doing some lightweight code reviews in class. This has sucked up a lot of time but I’m hoping that it ends up being worthwhile as a way to force students to keep revisiting and revising their code.

I’d appreciate pointers, suggestions, etc.

Around Hanksville Utah

Last weekend Sarah had a work trip so the boys and I spent a few days in the desert. The area around Hanksville–a tiny town right in the middle of Utah’s southeast quadrant that got electricity only in 1960–contains a lot of stuff I hadn’t seen yet, so we operated out of a motel there. Camping would have been more interesting, but I figured the short days and cold nights that we get in the high desert in late October might not be that fun.

Just northwest of Hanksville is an area of Mars-like badlands that I wanted to poke around in. Fittingly, this area contains the Mars Desert Research Station, a facility used by the Mars Society to let crews simulate being on Mars. That recent stupid John Carter movie had some scenes filmed not far away. Also nearby is the Hanksville-Burpee Dinosaur Quarry, a recently discovered treasure trove of fossil bones. Visiting this site turned out to be not that interesting; the people working there had taken a lot of care to hide their ongoing work under foil and sand, leaving only a few random (and presumably uninteresting) bones exposed. With any luck, next time we’ll be able to visit while they’re working.

I tried to explain to the boys the complex rules for collecting rocks and fossils which depend on what kind of land you’re on (BLM, wilderness study area, national park, national monument, etc.), who you are (land owner, person given permission by land owner, holder of mining claim, etc.), what methods you are using (collecting surface material, using hand tools, etc.), for what purpose you are collecting (personal use vs. commercial), type of material being collected (vertebrate fossils, invertebrate fossils, human artifacts, minerals, etc.), how much material you collect (“BLM regulations allow the collection of 25 pounds per day of petrified wood plus one piece, provided that the total removed by one person does not exceed 250 pounds in one calendar year”), etc. Of course at some point what happens is a boy rolls his eyes, holds up some pebble, and says “Dad… just tell me if I can take this rock home.”

On Saturday I had planned to spend the day exploring the area around Cowboy Cave, a (misnamed) alcove in a remote tributary of Horseshoe Canyon that was first inhabited by humans more than 8000 years ago. The bottom layer of organic debris in Cowboy Cave, 13,000 years old, contains dung from mammoth, bison, horse, camels, and sloth—it’s wild to think about these animals wandering around Utah. Also I have heard there are little-known dinosaur trackways nearby and I wanted to look for those. However, although the kids admitted that all of this sounded kind of cool, they were unimpressed by the prospect of 3 hours of driving on bumpy dirt roads and vetoed the plan.

We got up early and our first stop was a location near Caineville where I had read about zillions of fossil oyster shells weathering out of the shale. This turned out to be the case and we picked up a few souvenirs. After that I wanted to kill some time while the sun got higher so we’d have more light and warmth in a slot canyon, so we visited Little Egypt, a great area of hoodoos in the foothills of the Henry Mountains. It was a lot like a smaller Goblin Valley but without the people. We ended up having lunch there; for some reason the kids totally love backpacking food so I fired up the Jetboil and made us some Mountain House chili mac.

Just a few miles down the road from Little Egypt is a collection of popular technical slot canyons with a nasty reputation for narrowness. We hiked up Leprechaun Canyon from the bottom, stopping at a point where none of us felt comfortable continuing, and in any case it was so dark we’d have needed headlamps to do so. We had a funny moment where one of the boys, who had repeatedly proclaimed we had to stop and turn around, noticed that he had forgotten to remove his sunglasses.

On our last day I wanted something kind of short so we could do most of the drive home in daylight. Crack Canyon is one that I’ve wanted to see for some time but I got intimidated by some of the descriptions of its obstacles, so we headed for the easier Little Wild Horse and Bell canyons. It used to be the case that these canyons had a slightly remote feel but since I had last been there, the road to their trailhead had been paved and the toilet facilities improved. LWH is spectacular, easy, and easy to get to, making it the most popular canyon in the San Rafael Swell. Even so, thanks perhaps to getting a bit of an early start, we saw few people. We did the eight mile loop hike which ascends LWH through the San Rafael Reef, walks a couple of miles behind the reef, and then descends Bell Canyon. We hadn’t been to Bell before but it turned out to be totally great: it’s fairly short, contains great narrows, we saw no people, and there were numerous kid-sized obstacles that provided them with entertaining climbing problems. Next time I think we’ll just go up and down Bell and give the more popular canyon a miss. The only not-entertaining obstacles were a couple of 30′ sections of cold, muddy water knee-deep for me and with slippery and uneven footing. I managed to carry both boys over these sections.

How Did Software Get So Reliable Without Proof?

Tony Hoare’s 1996 paper How Did Software Get So Reliable Without Proof? addresses the apparent paradox where software more or less works without having been either proved correct or tested on more than an infinitesimal fraction of its execution paths. Early in the paper we read:

Dire warnings have been issued of the dangers of safety-critical software controlling health equipment, aircraft, weapons systems and industrial processes, including nuclear power stations. The arguments were sufficiently persuasive to trigger a significant research effort devoted to the problem of program correctness. A proportion of this research was based on the ideal of certainty achieved by mathematical proof.

Fortunately, the problem of program correctness has turned out to be far less serious than predicted. A recent analysis by Mackenzie has shown that of several thousand deaths so far reliably attributed to dependence on computers, only ten or so can be explained by errors in the software: most of these were due to a couple of instances of incorrect dosage calculations in the treatment of cancer by radiation. Similarly predictions of collapse of software due to size have been falsified by continuous operation of real-time software systems now measured in tens of millions of lines of code, and subjected to thousands of updates per year.

So what happened? Hoare’s thesis—which is good reading, but largely uncontroversial—is that a combination of factors was responsible. We got better at managing software projects. When testing is done right, it is almost unreasonably effective at uncovering defects that matter. Via debugging, we eliminate the bugs that bite us often, leaving behind an ocean of defects that either don’t manifest often or don’t matter very much when they do. Software is over-engineered, for example by redundant checks for exceptional conditions. Finally, the benefits of type checking and structured programming became widely understood during the decades leading up to 1996.

The rest of this piece looks at what has changed in the 16 years since Hoare’s paper was published. Perhaps most importantly, computers continue to mostly work. I have no idea if software is better or worse now than it was in 1996, but most of us can use a computer all day without major hassles. As far as I know, the number of deaths reliably attributed to software is still not hugely larger than ten.

Software, especially in critical systems, has grown dramatically larger since 1996: by a factor of at least 100 in some cases. Since the factor of growth was probably similar during the 1980-1996 period, it seems a bit odd that Hoare didn’t include much discussion of modularity; this would be at the top of my list of reasons why large software can work. The total size of a well-modularized software system is almost irrelevant to most developers, whereas even a small system can become intractable to develop if it is sufficiently badly modularized. My understanding is that both the Windows NT and Linux kernels experienced serious growing pains at various times when coupling between subsystems made development and debugging more difficult than it needed to be. In both cases, a significant amount of effort had to be explicitly devoted to cleaning up interfaces between subsystems. When I attended the GCC Summit in 2010, similar discussions were underway about how to slowly ratchet up the degree of modularity. I’m guessing that every large project faces the same issues.

A major change since 1996 is that security has emerged as an Achilles’ Heel of software systems. We are impressively poor at creating networked systems (and even non-networked ones) that are even minimally resistant to intrusion. There does not appear to be any evidence that critical software is more secure than regular Internet-facing software, though it does enjoy some security through obscurity. We’re stuck with a deploy-and-patch model, and the market for exploits that goes along with it, and as far as I know, nobody has a better way out than full formal verification of security properties (some of which will be very difficult to formalize and verify).

Finally, formal correctness proofs have not been adopted (at all) as a mainstream way to increase the quality of software. It remains almost unbelievably difficult to produce proofs about real software systems even though methods for doing so have greatly improved since 1996. On the other hand, lightweight formal methods are widely used; static analysis can rapidly detect a wide variety of shallow errors that would otherwise result in difficult debugging sessions.

NOTE: The article is behind a paywall so high that I couldn’t even get to it from on campus, and had to use interlibrary loan instead. I tried to find a way to read the fair use regulations in such a way that I could post a copy but this seems like too much of a stretch, sorry…

Blogs

I’ve been reading blogs since well before they were called blogs, though it was only fairly recently that I started using RSS to scale up the number of blogs I follow. I really enjoy the way this medium encourages unforced writing: people pretty much post whatever they’re thinking about right now. Below is the list of blogs I’m currently subscribed to. Am I interested in every random thought that every one of these people has? Not even remotely. But it is nice to be able to scroll past this stuff, picking and choosing something to read here and there. Correspondingly, I don’t make much of an effort to censor myself here; if a few people enjoy each post and everyone else skips over it, this isn’t a problem.

.mischief.mayhem.soap.
0xjfdube
33 Bits of Entropy
A Critical Systems Blog
ACM SIGBED – Special Interest Group on Embedded Systems
Across Utah
American Alpine Institute – Climbing Blog
An Academic’s Freedom
Andi Kleen’s blog
Andreas Gal
andybartlett.com
anil.recoil.org
apkudo
Arbitrary Thoughts
Arctic Sea Ice
Ars Experientia
Articles
Awkward Stock Photos
Azulsystems : Blogs » cliff
Backcountry Utah’s Outdoor Adventure Journal
Backyard Excursions
Bad Nomenclature
Beki’s Blog
ben’s blog
Better Embedded System SW
Bit9 – Activity
BLDGBLOG
Blogs
BonnevilleMariner.com
Brandon Sanderson Blog
Cassandra Van Buren, Ph.D.
Cedar & Sand
Charlie’s Diary
Chromium Blog
Code Love
codeslower.com
Colossal
command center
Comments on: Remote Education Final Project
Cooking For Engineers
Cool Tools
Cool Verification
CUSA Latest Rave
Dan Kaminsky’s Blog
Daniel’s Software Blog
Data Beta
Dave Nicolette
Dave’s Data
David A. Wheeler’s Blog
David Byrne’s Journal
David LeBlanc’s Web Log
DBMS Musings
DDI
dead reckon
Deprogramming
Desert Explorer
Dinochick Blogs
Division by Zero
e-Literate
Ed’s Blog
Edupocalypse Now
eighty-twenty news
Embedded Coding
Embedded Gurus – Experts on Embedded Software
Embedded in Academia
Eric Seidel
Errata Security
Everything and Nothing.
Faith & Farming
feed/http://carolineandpat.wordpress.com/feed/
Fell in Love with Data
Female Computer Scientist
Frama-C news and ideas
Fuck Yeah Fluid Dynamics
FYI News for Faculty & Staff » Info for Researchers
garfield minus garfield
Gear Review: The Ultimate Solo Tent « Trek Alaska – Hiking and …
Geek Prof
Gnome’s Lair
Gold Panning
Google Open Source Blog
Gowers’s Weblog
Gödel’s Lost Letter and P=NP
Hack Education
Hardwarebug
Hiking the Great American Southwest
Homesick Texan
How to Spot a Psychopath
Hyperbole and a Half
I, Cringely – Cringely on technology
Iain [M] Banks
Ian Bogost
Indistinguishable from Jesse
Industry Outsider
Inflatable Kayaks & Packrafts
Innovate.EDU
Inside 233
Interactive Theorem-Proving
interfluidity
it is NOT junk
It will never work in theory
Ivan Fratric’s Security Blog
Jay McCarthy
Jeff Epler’s blog
Jefferson’s Wheel
Jens Gustedt’s Blog
jg’s Ramblings
JOJILAND
Journal of a Programmer
Just Software Solutions Blog
keeping simple
Kelsey Publishing
Kevin Fu
KidSuperHiker
ladamic’s blog
Lambda the Ultimate – Programming Languages Weblog
Lana Yarosh
Landslide
lcamtuf’s blog
Lex Spoon
Links
LLVM Project Blog
logistic aggression
Lonnie Dupre
Lorenzo Martignoni
Love & Sex
Math-Blog
Mathematics and Computation
Michael Nielsen
microkerneldude
Miguel de Icaza
Moebius Strip
MormonLesbian
Musings by @txflygirl
My superpower is synchronicity
natural language processing blog
Nicholas Nethercote
Nick’s Blog
No Place Like Homes
Observations from Uppsala
Off The Lip
One Div Zero
pagetable.com
phed.org
Planet Pocket Tool
PostSecret
Preshing on Programming
Programming in the 21st Century
PSD : Photoshop Disasters 
Quetzalcoatal
Random ASCII
Random Observations
Raspberry Pi
realtimecollisiondetection.net – the blog
research!rsc
Retraction Watch
RockArt.me | Rock Art Photo Blog
Scott Tsai’s blog
Scotts World
Scouting NY
Scripts to Programs
Sean Heelan’s Blog
SemiAccurate
Sheryl’s Blog
Shtetl-Optimized
Sirikata
smitten kitchen
Snail in a Turtleneck
Sound & Fury
Sprouting the Beans
Spudd 64 / Matt Kish
Stack Overflow
Star Valley Weather
Steep Blog
Stephen Wolfram Blog
Steve Bennett blogs
Sticky Bits
still_exploring
StraightChuter.com – Backcountry Skiing & Beyond
Stupid Compiler
Summit42.com
SURVIVING IN ARGENTINA
Sutter’s Mill
Tagide
Tech Notes
tedherman’s posterous
Test Obsessed
The Changelog
The Chronicle of Higher Education | Advice
The Chronicle of Higher Education | News
The Digital Antiquarian
The Endeavour
The Flying Frog Blog
The Geomblog
The Homeless Adjunct
The Invisible Things Lab’s blog
The journey so far… 2007-2012
The Kid Should See This.
The Life of Bryan
The Little Calculist
The Oatmeal – Comics, Quizzes, & Stories
The Onion
The People’s Republic of Interactive Fiction
The Pursuit of Life
The Racket Blog
The Roaming Dials
The Shape of Code
The Spiced Life — Musings & Recipes From My Kitchen
The Third Bit
The Universe of Discourse
The Word of Notch
This is what a computer scientist looks like
Thoughts on software and systems engineering
Tom Moertel’s Blog
Toothpaste For Dinner
TvE 2100 – Home
Udacity
University of Utah
updated sporadically at best
UT Outdoors
Utah – News
Utah Arch
Utah Avalanche Center – Salt Lake
Utah Caves
Valve
Vintage Space
Virtual Now – Dan Hersey’s Blog
Visualization, etc.
Vivek Haldar
Volatile and Decentralized
Wasatch Citizen SkiMo Series
Wasatch Runner
Wasatch Weather Weenies
Wayne Hale’s Blog
We’re all fine here
Winning Race Conditions
WordPress News
www.linusakesson.net
Xi Wang
xkcd.com
xmonad
You Got to be Kidding’s Blog
zhiv
Zvonimir Rakamaric
  Bartosz Milewski’s Programming Cafe
♥ Brogramming Days ♥

EMSOFT 2012

I just got back from Tampere, Finland where I was one of the program chairs for EMSOFT, an embedded software conference. If I haven’t blogged about this much, it’s because I’m sort of a reluctant and not especially talented organizer of events. Happily, EMSOFT is just one third of the larger Embedded Systems Week, so logistics were handled at a higher level. Also happily, I had a co-chair Florence Maraninchi who did more than half of the work.

Visiting Finland was a pleasure; people were very friendly and the beer was good. On the other hand, Tampere wasn’t that easy to get to (~24 hours travel time from Salt Lake City) and my pessimistic expectations for October at 61°N were met: every day it was drizzly and not a lot above freezing. I saw the sun about once while in Finland, and by the time I left the days were noticeably shorter than when I arrived. I also hadn’t realized how far east Finland is: it’s only a four-hour drive from Helsinki to St. Petersburg. I found Finnish to be hilariously indecipherable, I hadn’t realized how much it differs from other European languages. I also hadn’t realized that everyone would just start speaking Finnish to me; apparently I fit in appearance-wise. Previously this has only happened to me in Germany and Holland. In general, however, everyone spoke perfectly acceptable English.

The conference was nice. Embedded software is a research area that I like a lot, though it can be a tricky one to appreciate due to a larger diversity of research approaches compared to other areas. For example, my view of OS research is that there’s a shared view for how to approach problems, even if there is a lot of variety in the actual problems being attacked. Embedded software isn’t like that. One of the topics we’ve started to see at embedded software conferences that I really like is looking at the robustness of software from the point of view of ensuring that bounded changes in inputs lead to bounded changes of outputs. This isn’t a notion that makes sense for all kinds of software, but it can be applied for example to feedback controllers and some kinds of signal processing codes. Robust control is an old idea but applying the technique to actual software is new. I’ve long believed that the lack of sensitivity analyses for software is a problem, so it’s great to see this actually being done.

University Economics and the End of Large Classes

I’ve been stalled on a draft of this piece for some time, but Amy Bruckman’s recent post provided the catalyst I needed to finish it up. She hypothesizes that “the future of universities is excelling at everything a MOOC is not.” Clearly universities can excel at activities that require students to be near each other and near professors, such as lab classes, motivating students by getting in their faces, and providing an environment for all of the extracurricular activities that make college such a great place to spend four or five years. A small set of universities such as Harvard also excels as an input filter and as a networking playground for the elite.

MOOCs—done right—should be able to improve upon the big lecture courses that all freshmen and sophomores suffer through at research universities. Even if MOOCs don’t produce better learning (they will be awesome for math and CS and physics, probably not so much for history or English) they are at least very cheap. So Bruckman is basically painting an idyllic picture where the students escape from the big lecture classes and also receive an improved amount of individual attention from instructors. From the professors’ side, we get to do the part of the teaching job that we enjoy and are good at: interacting with smaller groups of students via discussions, team work, and lab work.

But this vision has a problem: the big lecture classes bring in a huge amount of tuition relative to the costs of running them, whereas small classes taught by well-paid professors are not at all economical. See my previous post on this topic and consider that my department chair recently reminded the faculty about a long-standing (but apparently as-yet unenforced) policy that any undergraduate class with fewer than 15 students is subject to cancellation. Part of the problem is that R1 universities have evolved a system where professors have light teaching loads. For example, each year I am required to teach one big class, one medium class, and one small class; this is typical for a CS professor at a research school. In the small class, and probably in the medium class, I’m confident that I can do a much better job than a MOOC, but this is probably not the case for the large class. When I started teaching I didn’t mind the big classes and was in fact happy about the opportunity to reach lots of students at once. For various reasons, I’ve soured on these classes.

The point is that if large lecture classes are replaced by MOOCs, universities face a revenue collapse that will force a major restructuring. This could result, for example, in people like me being asked to cover a larger fraction of our salaries from grants. That is, the university could save money by covering only 50% or 25% of our salaries instead of the current standard arrangement where it pays 75%. Another possibility is that many professors are let go while others face much larger teaching loads. According to my university’s regulations, “A faculty member with tenure may be terminated or given a renewal contract with a substantially reduced status because of financial exigency”—which is what would happen following a revenue collapse. I think all universities have an analogous clause. Either of these changes would represent a major turn for the worse in American academic research. A third possibility is that universities will charge students to take credit hours obtained through a MOOC and count them towards a degree. This seems doubtful to work in the long run, but I’m guessing it is precisely what most of the universities allying with Coursera are hoping to do.

Some small college classes are extremely good and can even change people’s lives. These can’t be replaced using any foreseeable technology. On the other hand, large classes need to go. I loathed them as a student and despise them as an instructor. It’s very difficult to do a good job as a teacher, and in practice some significant fraction of the students students slips through without any reasonable mastery of the material. Combined with high tuition, this is a bad combination. The questions are: How to fix these classes and how to avoid throwing out the baby with the bathwater?

Of Course It’s an Interview

Arvind Narayanan wrote a mostly very good piece about some things that surprised him while interviewing for faculty jobs. One of them, “it’s not an interview,” was a surprise to me as well, since it’s wrong. There’s no doubt variation among individuals, but here are a few things I try to find out during a faculty interview.

Do you know why you’re here? Advisors often put pressure on their most promising students to go into academia, and some candidates arrive at the job interview for no better reason than a faculty position would be the latest in a series of stunning successes at meeting people’s expectations. I strongly prefer a candidate who understands and can articulate why he wants a faculty job.

Are you ready to be an authority figure? Professors have to run courses, degree programs, conferences, committees, research groups, and more. Managing people is difficult and requires a degree of maturity and finesse.

Are you a one-hit wonder? Although most people who interview for faculty positions have participated in several projects, it’s still usually the case that there’s one main body of work: the PhD thesis. Of course, that work was done under an advisor who, for all we know, supplied most of the ideas. The question is: Is the candidate creative enough, and does she understand the world deeply enough, that—working without a supervisor and working with students who will initially be very inexperienced—she can choose appropriate problems to attack in order to forge an identity as a strong, independent researcher?

Generally speaking, these questions can answered moderately better by a candidate who has done a postdoc and much better by a candidate with some industrial experience.

There’s more, but I think these three items get the idea across. If Dr. Narayanan aced his interviews without realizing what people were really asking, then more power to him. Most of us probably did the same thing. Even so, I don’t think “it’s not an interview” is what we want sitting out there as potential advice to the next generation of candidates.

I don’t bother trying to figure out if the candidate is an asshole. It is an iron law of assholes to never appear so to people with authority. This kind of information has to be teased out of recommendation letters or a back channel.