Swift's core team recently found out that they don't understand the type system they've created - they were fixing compiler 'bugs' for months without getting anywhere, until one of them finally realized hey, I should probably attempt to understand what we've built, not just 'fix' a never ending stream of bugs we seem to be having.
Turns out, the type system they built guarantees 100% that type checking is undecidable (in software developer terms, you can crash the compiler by typing perfectly legal Swift code and nobody at Apple knows how to fix it without breaking existing code because they didn't even know they built a language that has this property up until very recently). They figured this out after announcing a stable ABI by the way. Upon discovery, some of the core team members said the discovery was great/nice work.
It's not like we have people who use mathematics to prove properties of type systems without any shadow of a doubt or anything. I wonder how many of them are working on Swift or are employed at Apple, within their multi-billion dollar R&D budget... I wouldn't at all be surprised if the answer was zero, given that it was a software developer who knew a little math who made this discovery.