Yes, "every language" was glib. In any language we could avoid it, actually, by hiding division behind something that gave a Maybe or Option or similar. My point, though, was that his "Imagine..." was actually representative of virtually all of the languages that virtually all of us work in virtually all of the time. It is therefore a poor example of a way in which HW is different.
Sure, that would be a good reason to go there. I didn't mean to cast aspersions at dependent types. I was just confused/amused at the typical case being cast as a hypothetical.