Yeah but could it even be changed at this point? I'd imagine that once the ball gets rolling, changing any kind of formatting rules for a site with over a decades worth of (hundreds of thousands, tens of millions? ) of posts would be pretttty hard to get past committee
I would strongly favor writing a script that went through the database and rewrites existing comments from the old to new syntax; I believe in this case that's doable. And you would want to message it ahead of time of course. But with those things done I think it'd work fine, especially because I suspect virtually anyone who's gotten used to the HN formatting codes is already familiar with real markdown so it'd be a relatively painless transition.