Archive for the ‘software’ Category.

Program verification is not a silver bullet

Alan Shostack points out that
Alan Drexler is excited about the interesting AMS survey article
“Formal Proof” (Hales)
because of the prospects for program verification.

I think the article is better at inspiring hope about computer verification of proofs than about proof system verification of computers.

For balance one should read the still-persuasive May 1979 paper
“Social processes and proofs of theorems and programs” (De Millo, Lipton, Perlis).
The abstract:

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 programs make the formal verification process difficult to justify and manage. It is felt that ease of formal verification should not dominate program language design.

(Note that that there are lots of copies cached around the web if you don’t have an ACM Portal subscription.)

Desk Checking

Ole Eichhorn has written a great essay on “the lost art of desk checking,” sharing how slow and painful experiences with debugging led to habits of deliberate and careful pre-planning and checking.

My own parallel experiences: Okay, I’m doing to date myself here too. I’m also 49 years old, but didn’t start programming until Senior High. First experiences were with Basic on a Xerox Sigma 7 (thanks, Xerox), and a Wang 2200B. Not much learned there.

I learned more during summer vacations, when I paid real money to the University of Rochester to use their mainframe. I discovered that my first APL programs actually worked. I tried my hand at IBM 360 assembly language programming, but debugging was expensive – each assemble/link/run cost over $2. So I started editing the binary object decks on a keypunch instead, reducing the cost of a link/run to something under 80 cents.

While I followed the technology curve and have all the modern development environment power tools, there’s nothing like designing cleanly and understanding what’s going on. To quote Eichhorn:

To write code I just look at my screen and start typing, and to fix code, I just look at my screen some more and type some more. So now, finally, I‘m done with desk checking, right?

Wrong.

I desk check everything. Thoroughly.

And this, to me, is a major league black art which is lost to all those who didn’t have to hand-punch cards and wait a week for their deck to run. It is a lost art, but an essential art, because all the tools which make entering code and editing code and compiling code and running code faster don’t make your code better.

lcms speed

Note for other open source color management system users searching for more transform speed from the LittleCMS library:

Turning off the one-entry cache cuts 40% from runtime – unless you’re transforming large uniform blocks for which a one-entry cache is actually suitable.

Eliminating the general-purpose byte packing and unpacking functions and replacing them with inline encoding-specific equivalents cuts another 15% of runtime.

Compound savings: 49%, or 2x speedup, which is what someone claimed on an lcms mailing list once without providing the code.

Future work: The cached performance could be made better by observing that all the thread-safe memory locking I find in lcms-1.17 is unnecessary if you assume that thread-local caches on the stack are just fine. Forget the locking, and inline the cache comparisons. I had no need to implement it though, so this is only theoretical.

[If you found this by search engine and it helped you out, drop me a note.]

Systems programmers help people

Way back in the 1970s, I attended a banquet at RIT, for incoming or prospective students. My assigned seat placed me next to another intended Computer Science major.

I had cut my teeth in high school on some Basic programming (on a Xerox Sigma mainframe and a Wang 2200B), then self-taught myself APL and IBM/360 assembly language (paying for access at UR to an APL terminal, and editing object decks on the keypunch to save money while debugging assembly language programs).

My dinnermate at the banquet had had no such experience. So in choosing her major and concentration, she had to depend on the layman’s descriptions she heard during a college visit. You see, application programmers write programs that actually do things. Meanwhile, system programmers work on the operating system.

What’s an operating system? Well, it doesn’t do anything itself, it’s just there to help people write application programs.

Why did she choose Computer Science with a system programming concentration? “I like to help people.”

Books

Here are two books that I’m enjoying right now. Neither of them is hot off the presses, but I thought I’d put a good word for each nonetheless.

more Sarbanes-Oxley backlash

While discussing the current venture capital situation, Paul Graham points out

An experienced CFO I know said flatly: “I would not want to be CFO of a public company now.”

and

This law was created to prevent future Enrons, not to destroy the IPO market. Since the IPO market was practically dead when it passed, few saw what bad effects it would have. But now that technology has recovered from the last bust, we can see clearly what a bottleneck Sarbanes-Oxley has become.

As always, read the whole thing.

Summa Contra Program Rot

Dan Bricklin’s essay Software That Lasts 200 Years is provocative.

We need to start thinking about software in a way more like how we think about building bridges, dams, and sewers. What we build must last for generations without total rebuilding. This requires new thinking and new ways of organizing development. This is especially important for governments of all sizes as well as for established, ongoing businesses and institutions.

I don’t quite agree with the analogies, but I am provoked.
Rather than thinking of ways to make software stable and useful for the long haul, I think that the better perspective is that data is long-term, so data design, data formats, interoperability are the important issues. It does not matter whether I can run ancient programs, it matters that the valuable data can reliably be exported, imported, or directly accessed via ever-better tools. One way to ensure stability of infrastructure is to freeze the tools forever; the other is to be prepared to use a different tool every day.
The fact that I can move my weblog back-end from Radio to Movable Type to something else makes the data itself more stable and valuable, not less.

Programming Languages for the JVM

Robert Tolksdorf: Programming Languages targeted for the Java VM: there are a lot of them. It’s not just Jython any more. Thanks to
Sean McGrath for the link.

Comparison of open-source version control systems

Shlomi Fish (ONLamp): The New Breed of Version Control Systems compares
CVS,
Subversion,
GNU Arch,
OpenCM,
Aegis,
Monotone,
and the non-open-source BitKeeper. The conclusion:

You probably should not use CVS, as there are several better alternatives,
unless you cannot get hosting for something else. (Note that GNU Savannah provides hosting for Arch, and there is documentation for using it with SourceForge). You should also not use
the free version of BitKeeper because of its restrictions.

Other systems are nicer than CVS and provide a better working experience.
When I work in CVS, I always take a long time to think where to place a file or
how to name it, because I know I cannot rename it later, without breaking
history. This is no problem in other version control systems that support
moving or renaming. One project in which I was involved decided to rename
their directories and split the entire project history.

Mark Shuttleworth funds software development bounties

The founder of Thawte, Mark Shuttleworth, has many
thoughts on open source development and its funding,
based on his experience as the sponsor of the SchoolTool project.

So the risk is that a well-funded open source team that is NOT lead by someone with a personal interest in shipping the project will get distracted by other shiny tech toys and fail to actually ship something focused and constructive. How are we dealing with that in the current round of work on SchoolTool? First, I’m personally watching and asking the core team to focus on actual functionality. They assure me that their engine work is “done”, and that they are currently working on a usable tool that can be tested by schools. Time will tell. And second, we will shortly have a second, collaborating team, that will I hope also bring much of the engineering work into a more public forum.

Time will tell. These are expensive ways to learn, but I feel that the experiment is very much worth doing. There are lots of tools I would like to see developed in the open source world that developers have not yet done for themselves, and which I would be prepared to fund. Perhaps other philanthropists are in a similar position. We need to learn how to do this effectively, and the only way to learn is to try.

He has recently issued
bounties for work he’s like to see happen with his SchoolTool project, with Python, and with Mozilla.