It's interesting just how much of the debate in modern logic boils down to aesthetic preferences. On the other hand, I guess that if there were overwhelming practical advantages, there wouldn't be much to debate...

BTW, here's a "discussion paper" by Paulson and Leslie Lamport about typing in specification laguages from 1999: https://www.cl.cam.ac.uk/~lp15/papers/Reports/lamport-paulso.... Paulson represents the "pro-type" view, but note that since that paper was written, there have been developments in mechanised theorem proving of untyped formalisms, including in Lamport's own (TLA+).

I wouldn’t call it “aesthetics” per se.

More like “No free lunch.”

You can gain advantages, e.g. more complete compile time guarantees, but at disadvantages, e.g. greater program complexity, or longer compile times.

The subjectivity is whether the tradeoff is “worth” it.