I need none of that guarantee and all of the compilation speed along with a language where juniors in my team can contribute quickly. Different problem space.
> Types either represent the data or not
This definitely required, but is only really the first step. Where types get really useful is when you need to change them later on. The key aspects here are how easily you can change them, and how much the language tooling can help.
As you go further towards formal verification you get:
* More accurate / tighter types. For example instead of `u8` you might have `range(0, 7)` or even a type representing all odd numbers.
* Better compile time detection of bugs. (Ultimately you are formally verifying the program.)
* Worse type errors. Eventually you're getting errors that are pretty much "couldn't prove the types are correct; try again".
* More difficulty satisfying the type checker. There's a reason formal verification of software isn't very popular.
So it's definitely true that "more obnoxious types" exist, but Go is very far from the obnoxious region. Even something like Rust is basically fine. I think you can even go a little into dependent types before they really start getting obnoxious.
TL;DR, he's just lazy and doesn't really care about bugs.
No. two types can represent the same payload, but one might be a simple structure, the other one could be three or twenty nested type template abstractions deep, and created by a proc macro so you can't chase down how it was made so easily.