You raise an interesting point, but it is my understanding that Swift is by far not the only language that has a shaky foundation in terms of type theory. Other

You raise an interesting point, but it is my understanding that Swift is by far not the only language that has a shaky foundation in terms of type theory. Other type systems can at least be unsound, I don't know if any of them is undecidable. Even so, "undecidable" doesn't need to be a problem. It would be possible that the undecidable Swift program is such a random mess that nobody would be likely to write it by accident. However, it is worth looking into more practical aspects of how Swift's type system works, and there I share your concerns. Swift is the _only_ language I have ever used where I have ever seen the error message "the type checker was unable to infer the type of this expression" etc. - sometimes on dead simple code. Worse, I once tried to write an expressive, generic, functional framework, only to discover that it was completely unusable because the type errors that Swift returned were simply wrong and to fix it you had to put in type annotations in a bunch of places (without necessarily knowing where, just from the error messages), making the whole API extremely verbose and not particularly declarative anymore.