"Tooling can also go beyond types, though."By "tooling" there, I wasn't referring to static analysis. I meant things like type-directed name resolution, type-directed completion, Agda's "holes", and so on. Strictly, these do not rely on the type system being "a part of" the language, but they do rely on some degree of standardization on a particular type system for the tool to work (or work well).
"Interleaved calls to different types, for example, can be found through tooling."
I actually don't understand exactly what you mean here. You might be surprised what even pretty rudimentary type systems can find if you leverage 'em right, though - as I mentioned in that other thread, I track which threads access what resources, and which functions live on which threads, with C's type system unadorned by additional checks (I do use additional static analysis, it just is entirely unnecessary to catch this one).
"Well, I realize that is false. But the hoops all of the examples I have seen that types have to jump through to accomplish that aren't exactly pleasant.
"So, maybe my preference is just that tooling can give you many of the benefits of more advanced type systems, without having to have all of the boilerplate of it everywhere in the code."
Ironically, I think my C code has more annotations for my static analysis tool-of-choice than the C types. Certainly there are a lot of poor type systems, and a lot of languages that expose particular type systems poorly. Boilerplate type annotations are mostly unnecessary in languages with type inference.
As I've said elsewhere, though, your tooling may be "more advanced type systems". Splint, for instance, can enforce linear typing - something that is not a part of the type system laid out in the C standard (or that enforced by typical C compilers, even with warnings).
"At any rate, I should say thank you very much for keeping this dialog going. Been a blast!"
Yes, it's turned out great :)