What limitations of type systems are you talking about?
> When you say "set-theoretic types", I hear, "get rid of types, just give me logic".
A type theory/type system is a logic, so I don't really understand this point. https://en.wikipedia.org/wiki/Type_theory#Logic
The alternative I propose is simpler than you would think, and definitely simpler than type theory, but it is also very new: http://abstractionlogic.com . And of course, it doesn't come with a fixed algorithm for type checking, but going forward and in the age of AI, I think that will turn out to be an advantage.
Given the context of the original post, type theory at least has the benefit of actually existing in industrial languages in the form of a bunch of implemented and in-use type systems.
> It is limiting to have to under-approximate the mathematical universe via statically typed chunks before being able to talk about the objects in the universe, and the article just describes another instance of why that is problematic in practice.
>
> The alternative I propose is simpler than you would think, and definitely simpler than type theory, but it is also very new: http://abstractionlogic.com . And of course, it doesn't come with a fixed algorithm for type checking, but going forward and in the age of AI, I think that will turn out to be an advantage.
That's helpful in understanding where you're coming from, but now I'm even more perplexed--what you've linked to seems extremely theoretical. The closest to something my industrial programmer brain can grasp and read that I'd care about (in the context of the original post we're discussing) is https://obua.com/publications/automating-abstraction-logic/1..., which seems focused on theorem proving.
None of this is meant to suggest that I don't see the value in what you've linked to--it will take me some time to absorb, but I will take a closer look--but if you want to come into a discussion about a post like this one and criticize it, and more generally type systems, I think you'd be better off showing more directly how your approach can solve the same problem (or how it doesn't need to solve it, which it sounds like you're implying) in a way that doesn't take reading through a bunch of fairly abstract posts and papers or watching a five-part video series first. And if there's no actual implementation (that I can see at least) then don't expect me, an industrial programmer--like most folks on HN I would guess vs. e.g. lambda-the-ultimate or whatever--to consider it worthwhile past idle curiosity.
I see value in Valim's post because it identifies a problem with type systems that I understand and have encountered, and provides an incremental and pragmatic solution to that. It doesn't seem like you're offering a coherent, practical alternative, regardless of the validity of your arguments ("It is limiting to have to under-approximate the mathematical universe via statically typed chunks before being able to talk about the objects in the universe" makes intuitive sense to me in this context, at least).
There are no tools for abstraction logic right now. I hope there will be in 15 months ;-) Maybe check back then.
