![[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.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2011-05-12 10:09 pm (UTC)From:i like the word "useful" when talking philosophy. "is this a useful question to be asking?" and "is this a useful answer to the question?" are good to say to stay on track; often they would be followed by "well, what's the intended use to begin with?". (i used this trick a few days ago when discussing the inherent value of original vs forged art and descartesesque notions of perceived reality.)
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.
this totally happened with my bread knife and that pineapple at dinner yesterday. (i get that the article means if you are showing off your knife, you'd better eventually want to eat pineapple.)
no subject
Date: 2011-05-12 10:17 pm (UTC)From:no subject
Date: 2011-05-13 01:31 pm (UTC)From:"what PL wants" seems super squishy because i don't think there is any one thing that PL can want. i think you need to divide it before you can make bottom line distinctions like that. the clearest statement i have seen is "make software creation better", but 'better' is complicated. safer? easier? more accessible?
no subject
Date: 2011-05-14 05:49 am (UTC)From: