[pvillano]

This stack exchange answer talks about the importance of decidability in type checking

https://langdev.stackexchange.com/a/2072

My interpretation

Decidability is of academic interest, and might be a hint if something is feasible.

But there are (1) ways of sidestepping undecidability, e.g. A valid C++/Rust program is one for which the typechecker terminates in x steps without overflowing the stack

And (2) things which are decidable, but physically impossible to calculate, e.g the last digit of the 10^10^10 th prime

What matters is being able to reject all incorrect programs, and accept most human written valid programs

[penteract]

Decidability of a type system is like well-typedness of a program. It doesn't guarantee it's sensible, but not having the property is an indicator of problems.

[kingstnap]

I'm not entirely smart enough to connect all of these things together but I think there is a kind of subtlety here thats being stepped on.

1. Complete, Decidable, Well founded are all distinct things.

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.

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.

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.

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. https://en.wikipedia.org/wiki/Aczel%27s_anti-foundation_axio...

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....

[pvillano]

But like, of all the expressive power vs analyzability trade-offs you can make, there's a huge leap in expressive power when you give away decidability.

Undecidability is not a sign that the foundation has cracks (not well founded), but it might be a sign that you put the foundation on wheels so you can drive it at highway speeds, with all the dangers that entails.

It's not a trade everyone would make, but the languages I prefer do.