I just have a couple of nitpicks that I'll offer along with my apologies for my forgetfulness.

I'm happy to have your comments now :)

Algorithms people, on the other hand, are sometimes distressingly vague about their choice of formalism, even when their theorems depend crucially on the formalism they're using.

That is exactly Lamport's complaint, going back to the '70s. But the difference is that he simply requires precision, not a specific formalism.

Erm, not really. Higher order logic has a pretty clear definition as opposed to first order logic.

That's not what I meant. You cannot tell whether an object is a first- or second-order logic without knowing the order of the formalism. A set can be first order in ZFC, but second-order in first-order PA.

And TLA+ uses first order logic.

Not exactly. Wait for part 2, but TLA+ formulas are first order, but propositions may be second-order (as well as modules).

You often imply that classical math is in some way simpler or easier that constructive math, but that's not a supportable claim.

My claim isn't absolute, but holds, I think, in the current state of affairs. As to constructive vs. non-constructive proofs, you may be right, but there's hardly a difference when it comes to software. The domains of most propositions are such that LEM holds even in constructive logics.