Hi Burak, all serious discussions about types end up talking about logic at some point, and I just don't think that types are a particularly helpful way to think about logic. I'd rather use normal mathematics to think about logic. Take a look at [1], at this point abstraction logic is less confused and hopefully clearer than it was a few years ago when you first checked it out.