Let xs be a finite list of natural numbers.
Let xs’ be the list that is xs sorted ascendingly.
I could write down in full formality, what it means for a list to be sorted, without ever talking at all about how you would go about calculating xs’ given xs. That is the power I am talking about. We can say what something is, without talking about how to get it.
And yes this still applies for constructive logic, Because the property of being sorted is just the logical property of a list. It’s a definition. To give a definition, I don’t need to talk about what kind of algorithm would produce something that satisfies this condition. That is completely separate.
And being able to see that as separate is a really useful abstraction, because it hides away many unimportant details.
Computer Science is about how-to-do-X knowledge as SICP says. Mathe is about talking about stuff in full formal detail without talking about this how-to-do-X knowledge, which can get very complicated.
How does a modern CPU add two 64-bit floating-point numbers? It’s certainly not an obvious simple way, because that would be way too slow. The CPU here illustrates the point as a sort of ultimate instantiation of implementation detail.
I kind of see what you’re saying, but I also rather think you’re talking about specifying very different things in a way that I don’t think is required. The closer CS definition of math’s “define a sorted list” is “determine if a list is sorted”. I’d argue it’s very close to equivalent to the math formality of whether a list is sorted. You can argue about the complexity behind the abstraction (Math’s foundations on set theory and symbols vs CS library and silicon foundations on memory storage and “list” indexing), but I don’t think that’s the point you’re making.
When used for different things, they’re very different in complexity. When used for the same things, they can be pretty similar.
Yes, that is a good point. I think you can totally write a program that checks given two lists as input, xs and xs’, that xs’ is sorted and also contains exactly all the elements from xs. That allows us to specify in code what it means that a list xs’ is what I get when I sort xs.
And yes I can do this without talking about how to sort a list. I nearly give a property such that there is only one function that is implied by this property: the sorting function. I can constrain what the program can be totally (at least if we ignore runtime and memory stuff).
Let xs be a finite list of natural numbers. Let xs’ be the list that is xs sorted ascendingly.
I could write down in full formality, what it means for a list to be sorted, without ever talking at all about how you would go about calculating xs’ given xs. That is the power I am talking about. We can say what something is, without talking about how to get it.
And yes this still applies for constructive logic, Because the property of being sorted is just the logical property of a list. It’s a definition. To give a definition, I don’t need to talk about what kind of algorithm would produce something that satisfies this condition. That is completely separate.
And being able to see that as separate is a really useful abstraction, because it hides away many unimportant details.
Computer Science is about how-to-do-X knowledge as SICP says. Mathe is about talking about stuff in full formal detail without talking about this how-to-do-X knowledge, which can get very complicated.
How does a modern CPU add two 64-bit floating-point numbers? It’s certainly not an obvious simple way, because that would be way too slow. The CPU here illustrates the point as a sort of ultimate instantiation of implementation detail.
I kind of see what you’re saying, but I also rather think you’re talking about specifying very different things in a way that I don’t think is required. The closer CS definition of math’s “define a sorted list” is “determine if a list is sorted”. I’d argue it’s very close to equivalent to the math formality of whether a list is sorted. You can argue about the complexity behind the abstraction (Math’s foundations on set theory and symbols vs CS library and silicon foundations on memory storage and “list” indexing), but I don’t think that’s the point you’re making.
When used for different things, they’re very different in complexity. When used for the same things, they can be pretty similar.
Yes, that is a good point. I think you can totally write a program that checks given two lists as input, xs and xs’, that xs’ is sorted and also contains exactly all the elements from xs. That allows us to specify in code what it means that a list xs’ is what I get when I sort xs.
And yes I can do this without talking about how to sort a list. I nearly give a property such that there is only one function that is implied by this property: the sorting function. I can constrain what the program can be totally (at least if we ignore runtime and memory stuff).