I must confess it has been a while since I last looked at this aspect of things on Linux... If harfbuzz is used by all of those it must be pretty complete by now - we'll have to do some digging and researchPango actually uses HarfBuzz on Linux for "complex text rendering" (http://www.pango.org), but since HarfBuzz is being used by GNOME, Firefox, Chrome OS, and Chrome, it's probably a safe bet I wish I had known about it back when I was writing my own toy game engine.
Hehe - oh that would be nice. I know the world of code-proving and such has moved on substantially in the last few years (particularly as efficient and freely available implementations of the boolean satisfiability algorithm now exist), however I'm not sure quite what the frontier of such research has produced as yet in terms of production-quality tools (I've not had the time in recent years to keep up with it). Not entirely related, but LLVM has a sub-project for 'symbolic execution' which essentially runs a program abstractly and attempts to tell you all the ways it might break... Unfortunately, I think the engine might be a bit big for that at present (well, unless someone wants to gift us a suitably sized super-computer)I have hit a bug with layout() not being called when it should have been causing an infinite loop, but I suspect it's because clearzeros isn't setting the dirty flag. Debugging this could be very difficult. It would be very nice to have some kind of code proving engine with constraints saying something like "whenever this changes, this needs to be called before this is called" and have it tell me the sequence of events when something breaks...
By the way, do you want to send a pull-request for the paragraph optimization you made? The commit you posted looks pretty solid, we could test it out on the 'develop' branch for the next major release if you want... See if anyone manages to break it.