6 ms·
ITP is a key part and a good start but I wouldn't call it the ultimate tool. Thought is more than logic. Logic operates on a model, after things have been name
by closedloop129 4y ago
ITP is a key part and a good start but I wouldn't call it the ultimate tool.
Thought is more than logic. Logic operates on a model, after things have been named and conceptualized. As the saying goes, there are two hard things in computer science, and ITP doesn't cover all of them.
- practal 4y agoI would say it covers naming things and cache invalidation. And it is really really good at avoiding off-by-one errors.
- jolux 4y agohow does it cover naming things?
- practal 4y agoThat depends on the ITP system. But in general, in an ITP system you can separate the name of something from how it is displayed. In the ITP system I am currently building, Practal, the displayed syntax does not need to be unique. So choosing a unique name becomes simpler, because you don't have to worry so much about how it looks, because that can be entirely different and doesn't need to be unique. Apart from that, every accessible element of your mathematical universe already has a name: it is the term you use to describe it.
- beckingz 4y agoSure you can rename things easily, but NAMING something CORRECTLY is hard, in an ontological sense where you may not know what the thing's name is until you truly know what it is.
- jolux 4y agoI've never thought that "naming things" meant keeping track of the name or anything, but that's hard too. I've always thought it meant the descriptive aspect of naming.