One thing which perhaps is not captured well in the article, is that rather unlike when reading/writing source code, where stepping through lines of code is a relatively uncommon task only done debugging. For interactive theorem provers it is a given. He discusses the bottom up & top-down approach to the solving goals with tactics & otherwise, but typically in both cases you will be stepping through expressions to get a better understanding. They generally aren't written to be read from just the source text alone.