3 ms·

I'm not convinced that it's feasible to design a language that way because features and the underlying system generally seem to influence each other so much, so

I'm not convinced that it's feasible to design a language that way because features and the underlying system generally seem to influence each other so much, so that I'd suspect starting with 'what you want' has a good chance of making the system unworkable due to breaking something like computationality or making classical logic unsound while making it very hard to notice (if it's not a theoretical property, then something more practical could also be problematic. Something like automation isn't a panacea either because a system needs to be amenable to it). Extending existing systems with something like intersection types seems already hard enough. As an example, it's very hard for me to judge what it means for equality to not have a type without an underlying system to go along with it. Since it's still featured as part of types (such as your dom f = A ∧ cod f = B example), you still need a typing rule, but what would that look like? It's at the very least non-obvious to me that this doesn't potentially have some issues. Or, what does extensionality for types cover that isn't done by subtypes? And should this just be a metatheoretic property, or also something that can be stated inside the system? Besides that, the current items on the list are of course reasonable enough (though nil strikes me as a regression from option types and paraconsistent logic strikes me as totally unusable in the general case as you'd lose A \/ B, ~A |- B, which is absolutely essential.)

practal 5y ago
You don't need a rule system to understand what equality is. Yes, it is not computational for sure. It's a logic, not a programming language. Nil is the way undefinedness is handled in Practal. It is the most elegant way I can think of. You can still have your option type, just as you can have Kleene logic operators, but these are more suitable for doing program verification work in Practal, not so much for doing general mathematics in Practal. You really want (T ∪ Nil) ∪ Nil = T ∪ Nil here, while in programming you usually don't want Option[Option[T]] to be the same as Option[T]. I am not saying it is easy to make all of this work, and to make it work soundly. But less just doesn't cut it. With a kernel-based approach, you have a chance to get it right. If you find an inconsistency, fix the kernel, and move on. Automation works just on top of it, and doesn't affect soundness. This is the great thing about automation in kernel-based ITP: If it finds some solution or counter-example, great. Otherwise, no harm done.

practal 5y ago

You don't need a rule system to understand what equality is. Yes, it is not computational for sure. It's a logic, not a programming language. Nil is the way undefinedness is handled in Practal. It is the most elegant way I can think of. You can still have your option type, just as you can have Kleene logic operators, but these are more suitable for doing program verification work in Practal, not so much for doing general mathematics in Practal. You really want (T ∪ Nil) ∪ Nil = T ∪ Nil here, while in programming you usually don't want Option[Option[T]] to be the same as Option[T]. I am not saying it is easy to make all of this work, and to make it work soundly. But less just doesn't cut it. With a kernel-based approach, you have a chance to get it right. If you find an inconsistency, fix the kernel, and move on. Automation works just on top of it, and doesn't affect soundness. This is the great thing about automation in kernel-based ITP: If it finds some solution or counter-example, great. Otherwise, no harm done.