But why dependent types and not one of the many other formal methods that have been around for decades? Especially given the trend towards compilation speed being a relevant design choice (e.g., golang).

Sound global formal verification largely sucks. Type checking is about as far as we've ever gotten using it for widespread real world applications, and most type checkers in major languages are only "sound-y".