![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
this n-category cafe article on the mathematically "sacred" and "profane", while not particularly coherent, makes a bunch of really interesting points.
first there is this sociological observation about how mathematicians get to know each other:
this clip doesn't really draw a distinction between a personal bottom line, though, and that of one's entire field. in terms of personal bottom lines, this rings true for me; the academic conversations i have typically go much better if we get each other's bottom lines out of the way (e.g. i might tell someone i want a programming language for IF, or a type theory for checking asymptotic complexity, or a clean setting where dependent functional and logic programs interoperate). but i'm not sure i could define what the research programme i associate with carries as its bottom line to the tune of "To the algebraic geometers of the sixties, the bottom line was the proof of the Weil conjectures." certainly for complexity theorists, the obvious bottom line is P vs. NP. but type theorists don't have an analogous sought-after result or theory to nail down -- maybe everyone has their pet problem (concurrency, interactivity, space usage, modularity, theorem proving) for which there is some hypothetical "holy grail" language, but certainly we aren't very unified about it. maybe this is part of the solidarity (and consequently marketing) problems that the PL community seems to have, perpetually; we can never really agree on what we're after.
the side remark about "duty" also struck me:
at first this bothered me, because i wanted to object, "but who assigns you this duty? that itself is a choice" -- until i recast it as a description of how to execute proof search. suppose you have a bunch of clauses in your context and some goal C. any clause with C at its head is "right", but there may be many. any clause that is a precondition to such a clause is "useful", but only because it's an intermediate step. the only way to decide what part of your context to use is to give an algorithm like focusing which forces you to pick, and to follow through on your choice. :P
maybe this can be applied to life as well: the only thing that can really justify an action is a pre-determined choice procedure, and having one, even if it's poor, is better than arbitrarity.
also i think the line "If I show you how my new knife cuts through some wood, I may do so to allow you to admire the sharpness of the blade, rather than because I want two pieces of wood." is good to keep in mind for any discussion of math/programming.
first there is this sociological observation about how mathematicians get to know each other:
When two mathematicians meet and feel out each other’s knowledge of mathematics, what they are really doing is finding out what each other’s bottom line is.
this clip doesn't really draw a distinction between a personal bottom line, though, and that of one's entire field. in terms of personal bottom lines, this rings true for me; the academic conversations i have typically go much better if we get each other's bottom lines out of the way (e.g. i might tell someone i want a programming language for IF, or a type theory for checking asymptotic complexity, or a clean setting where dependent functional and logic programs interoperate). but i'm not sure i could define what the research programme i associate with carries as its bottom line to the tune of "To the algebraic geometers of the sixties, the bottom line was the proof of the Weil conjectures." certainly for complexity theorists, the obvious bottom line is P vs. NP. but type theorists don't have an analogous sought-after result or theory to nail down -- maybe everyone has their pet problem (concurrency, interactivity, space usage, modularity, theorem proving) for which there is some hypothetical "holy grail" language, but certainly we aren't very unified about it. maybe this is part of the solidarity (and consequently marketing) problems that the PL community seems to have, perpetually; we can never really agree on what we're after.
the side remark about "duty" also struck me:
…of the three reasons for choice [because it is useful; because it is right; and, because it is my duty], the third alone is a complete reason. Choice is always choice to do an individual action. Why do I do it? The answer ‘because it is useful’ explains only why I do an action leading to a certain end: not why, among the various possible actions which might have led to that end, I choose this and not another. The answer ‘because it is right’ explains only why I do an action of a certain kind, specified by the rule which I obey; not why, among the various possible actions conforming to that specification, I choose this and not another. But the answer ‘because it is my duty’ is a complete answer.
at first this bothered me, because i wanted to object, "but who assigns you this duty? that itself is a choice" -- until i recast it as a description of how to execute proof search. suppose you have a bunch of clauses in your context and some goal C. any clause with C at its head is "right", but there may be many. any clause that is a precondition to such a clause is "useful", but only because it's an intermediate step. the only way to decide what part of your context to use is to give an algorithm like focusing which forces you to pick, and to follow through on your choice. :P
maybe this can be applied to life as well: the only thing that can really justify an action is a pre-determined choice procedure, and having one, even if it's poor, is better than arbitrarity.
also i think the line "If I show you how my new knife cuts through some wood, I may do so to allow you to admire the sharpness of the blade, rather than because I want two pieces of wood." is good to keep in mind for any discussion of math/programming.
