4 ms·

Yes, a type theory is a logic, but not a particularly good one. It is limiting to have to under-approximate the mathematical universe via statically typed chunk

Yes, a type theory is a logic, but not a particularly good one. 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 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.

ddellacosta 2y ago
> Yes, a type theory is a logic, but not a particularly good one. 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 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/ 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).
- practal 2y ago
  How much work you want to put into understanding abstraction logic is very much up to you. There are no tools for abstraction logic right now. I hope there will be in 15 months ;-) Maybe check back then.
  - josevalim 2y ago
    While it is a bit unfortunate that the time spent to write the article continues to be used as a criticism, and perhaps as a dig, I’ll only add that I have no formal background on type theory or logic. So much of the 15 months was also spent on learning the underlying concepts, mostly on my free time, and I am quite happy to even produce _something_ on a topic I have only recently got into. I am sure people smarter or more familiar with the theory than me would produce more in less time.
    - practal 2y ago
      No, I was just joking in my last comment, as I know how time-consuming true progress can be. I'm also familiar with how type theory can overcomplicate simple things. When I see this happening, I can't help but point it out, although my criticism might seem out of context. I would be very happy if I could deliver tools for abstraction logic in just 15 months.

ddellacosta 2y ago

> Yes, a type theory is a logic, but not a particularly good one. 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 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/ 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).

practal 2y ago
How much work you want to put into understanding abstraction logic is very much up to you. There are no tools for abstraction logic right now. I hope there will be in 15 months ;-) Maybe check back then.
- josevalim 2y ago
  While it is a bit unfortunate that the time spent to write the article continues to be used as a criticism, and perhaps as a dig, I’ll only add that I have no formal background on type theory or logic. So much of the 15 months was also spent on learning the underlying concepts, mostly on my free time, and I am quite happy to even produce _something_ on a topic I have only recently got into. I am sure people smarter or more familiar with the theory than me would produce more in less time.
  - practal 2y ago
    No, I was just joking in my last comment, as I know how time-consuming true progress can be. I'm also familiar with how type theory can overcomplicate simple things. When I see this happening, I can't help but point it out, although my criticism might seem out of context. I would be very happy if I could deliver tools for abstraction logic in just 15 months.