| > 2. Zig (which allows types to be types) is Turing complete at compile time regardless. So the compiler isn't guaranteed to halt regardless and it doesn't practically matter. Being Turing complete at compile time causes the same kinds of problems as undecidable typechecking, sure. That doesn't make either of those things a good idea. > 3. The existance of a set x contains x is not enough by itself to create a paradox and prove false. All it does is violate the axiom of foundation, not create a russles paradox. A set that violates an axiom is immediately a paradox from which you can prove anything. See the principle of explosion. > 4. The axiom of foundation is a weird sort of arbitrariness in that it implies this sort of DAG nature to all sets under set membership operation. Well, sure, that's what a set is. I don't think it's weird; quite the opposite, > 5. This isn't nessesarily some axiomatically self evident fact. Aczel's anti foundation axiom works as well and you can make arbitrary sets with weird memberships if you adopt that. I don't think this kind of thing is established enough to say that it works well. There aren't enough people working on those non-standard axioms and theories to conclude that they're practical or meet our intuitions. > 6. The Axiom of Foundation exists to stop you from making weird cycles, but there is parallel to the axiom of choice, which directly asserts the existance of non computable sets using a non algorithmicly realizable oracle anyway.... The Axiom of Foundation exists to make induction work, and so does the Axiom of Choice. They both express a sense that if you can start and you can always make progress, eventually you can finish. It's very hard to prove general results without them. |