Follow up. >> 3. No directories, just a global scope. Yes, this is a drawback in my >> eyes, too. But this is not an easy task as it seems at first sight. If >> you take this idea seriously, i.e. topics are finally independent, you end >> up with a need for a linker infrastructure. Compare to compiler.
> I'm sympathetic to this complaint. Indeed, when we discussed the > "usage is discouraged" I recommended more information to provide > information hiding. I don't think it's complicated to do, and I think it'd > could be a good idea, though of course the devil's in the details. Let me first explain, why I think breaking up the whole file into pieces along the borders of topics is not enough. The main reason for this is allowing diversification. We already see that an alternative to ZFC, intuitionistic logic, is developed in parallel. And in my mathbox you find propositional logic based on Lukasiewicz axioms. It would be nice to let higher abstraction levels of mathematics (I call them modules here) depend on whatever foundations the user requests. In such a situation there is need for a descriptive layer that programmers call interface. The module declares what prerequisites must be fulfilled to be valid, and other, more foundational modules, provide this demands. The idea is to let modules be interchangeable. Such a situation is already solved by programming infrastructure, and programs that check the validity and compatability of interfaces are called linkers. In my eyes advanced forms of Metamath should feature such an infrastructure. The good news is, that this problem is already solved, and we just have to adapt an existing solution. The bad news is, the amount of work to adapt this solution appears still daunting to me. Wolf Lammen -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/427a04e3-a56e-4689-8ca2-634636f28e4b%40googlegroups.com.
