Jon Sterling on Nostr: Apropos nothing, I just want to say that I find coding in Cubical Type Theory very ...
Apropos nothing, I just want to say that I find coding in Cubical Type Theory very frustrating 🤣
I spent several years of my life trying to find ways to make it less frustrating. I think we had some interesting ideas. Do I think that some kind of Cubical Type Theory is the answer? I would say that it could be, but I think a lot will have to change in the meanwhile for it to be seriously usable.
I think it is good that we have early adopters who are developing a lot of great code, building up expertise and experience. This is definitely the kind of accumulation of wisdom that we will need in order to take the next steps forward. At the same time, I want us to not lose track of the fact that many of the things we are willing to put up with as early adopters are not acceptable in general — and this is not a “blub vs. lisp” situation where I am trying to appeal to the mythical uncultured Joe Programmer, but rather more of a “blub vs. INTERCAL” situation.
I spent several years of my life trying to find ways to make it less frustrating. I think we had some interesting ideas. Do I think that some kind of Cubical Type Theory is the answer? I would say that it could be, but I think a lot will have to change in the meanwhile for it to be seriously usable.
I think it is good that we have early adopters who are developing a lot of great code, building up expertise and experience. This is definitely the kind of accumulation of wisdom that we will need in order to take the next steps forward. At the same time, I want us to not lose track of the fact that many of the things we are willing to put up with as early adopters are not acceptable in general — and this is not a “blub vs. lisp” situation where I am trying to appeal to the mythical uncultured Joe Programmer, but rather more of a “blub vs. INTERCAL” situation.