thoran

On the other hand, when you do have categories in a language and not the smartest people in the language's community, you do have real problems: You end up with conflicting definitions of homonymic methods because every one wants his own "toJson" crap. And everyone tries to monkey patch every other components. Ruby is plagued by this disease.

Haxe and Scala (and probably many others) have a nice solution to this problem. You can add "methods" to existing classes but only you can see them. You never really change the semantic of something that does not belong to you.

It's my fault, I think I read your answer too quickly and miss a negation somewhere.

So, yes, a formal rewriting of Wiles' proof is "only" a practical challenge. But a big one. Just about 15 years ago, we were just able to prove the Fundamental theorem of algebra in Coq (a 200 years old theorem that is routinely taught to undergraduates).

No, you're wrong. This is not a theoretical issue there, but a practical one.

Almost all mathematics (and this certainly includes Wile's proof) could be written in Coq, in theory. It is extremely hard to do in practice.

Mathematicians write proof for their peers who have a smart brain. Most of the trivial and less than trivial details are omitted. Coq cannot not accept this (because he is very stupid and can't figure the missing steps). It turns out that it is particularly hard and boring to fill the missing holes in a "human" proof.

Gödel comes in when you try to prove Coq's correctness within Coq (but this was partially done, in a sense)

On MacOS, you would distribute a library as a 'Framework' (a package containing the binary shared object, headers, documentation, resources, sub frameworks...). In Xcode, you can quickly add a framework dependency. And if you need to modify the framework too, you can use “sub projects” (the sub project build the framework you are using in the super project). With recent Xcode versions, it works reasonably well. In this world, you don't need CocoaPods at all. Everything is nicely compositional. You would have expected that they had extended this mechanism when they introduced the iPhone?

But they manage to totally screw that. First of all, they drop the support for Frameworks!! So if you want to ship a cross platform (MacOS/iOS) library, you must maintain two targets (one static lib for iOS (and good luck to manage its inner resources), one framework for MacOS). You also have to be careful to have compatible architecture between the sub project and the parent project, a problem that is aggravated by the multiplication of iOS architectures (armv 5, 6, 7, 8, 9, ...). Apparently, forwarding the required architectures from a parent project down to its dependant sub projects is a very difficult problem...

Then, the community feels the need to fix this mess to have a working environment where you can easily share your work: CocoaPods was born.