Yes, and to be clear I have never encountered these issues on practical problems. I am also not claiming Kotlin has or lacks these properties, just pointing out the fact if you care about toolability, soundness and decidability are important factors to consider and if there is a language design issue, it makes me less confident in any tooling which is built around it.
It comes down to whether you want type checking to work all the time, or most of the time? If your answer is "most of the time", then just use a dynamically typed language with GPT-based autocompletion. Most of the time completion and refactoring will work just fine.
Re: type checking in C#, maybe try the following example?
a) "most of the time" being 60% (very roughly what I'd expect when doing renaming beyond a single function in JS, and that's being optimistic).
b) "most of the time" being 99% (very roughly what I'd expect in a typical C#/java/kotlin codebase that isn't using too much reflection).
Even aside from that, I'd argue that nullability, array covariance, and reflection all have MUCH bigger practical impacts on typechecking reliability than Turing-completeness. Most languages will simply fail to compile if the computed types require too much recursion, making the issue relatively moot.
Type-checkers don't actually need to solve the halting problem to be sound, they just need to guarantee completion for _most_ types of code, and anything that can't be guaranteed can simply be rejected.
I would expect this number to get closer to 99% with LLM-based AI code completion tools, so the gap between dynamically-typed languages and "good enough" languages that claim to be statically typed (but are in fact unsound) will become much less significant. But if you want correctness, you will need stronger guarantees.
> I'd argue that nullability, array covariance, and reflection...
I would mostly agree with that statement, with the caveat that it depends on what you want from your type system. Personally, I want the checker to be (1) sound and (2) decidable and (3) fast. For everything else there's runtime type checking.
> Type-checkers don't actually need to solve the halting problem to be sound, they just need to guarantee completion for _most_ types of code
Although I don't see much difference between undecidable type systems and dynamically typed languages, as I wrote, I see undecidability as less of an issue. My main concern is unsoundness, which is more critical and unclear how to fix. By "soundness" I specifically mean the formal property that "well-typed programs cannot go wrong". "Most types of code" is just a statistical claim, in which case you might as well use Python or JS/TS with a linter. Too many statically-typed languages decide to go off and roll their own types without reading PL literature, then end up with dealing with these issues later down the line.
> It comes down to whether you want type checking to work all the time, or most of the time? If your answer is "most of the time", then just use a dynamically typed language with GPT-based autocompletion. Most of the time completion and refactoring will work just fine.
This is bad advice. Such an approach will go wrong often enough to burn you, and it will go wrong silently, whereas the kind of issues you describe tend to lead to something far more visible (and therefore correctible) like a complier internal error or an IDE refusing to perform a refactor.
It comes down to whether you want type checking to work all the time, or most of the time? If your answer is "most of the time", then just use a dynamically typed language with GPT-based autocompletion. Most of the time completion and refactoring will work just fine.
Re: type checking in C#, maybe try the following example?
https://learn.microsoft.com/en-us/archive/blogs/ericlippert/...