"algorithm discovery" / how to capture human reasoning

[gusl]

GusLacerda: I went to a talk by Pfenning on Friday
GusLacerda: and asked him about who here does AR [automated reasoning]
GusLacerda: and the answer was disappointing
GusLacerda: basically, people who are into type theory
aCleverEpithet: yes
GusLacerda: I told him I was interested in "algorithm discovery"
GusLacerda: this was 50% bullshit
GusLacerda: because "algorithm discovery" is a non-existent research area
GusLacerda: but he seemed interested
GusLacerda: I explained the idea... which he and one student seemed to get excited about
aCleverEpithet: it is interesting
GusLacerda: but his conclusion, as far as collaborators go, was: Herb Simon is dead...
[note: to be fair, he did tell me to check out Raul Valdes-Perez, which is a very good lead. Is this guy actually at CMU?]
aCleverEpithet: hard, but interesting
aCleverEpithet: this is true
GusLacerda: everyone says this
GusLacerda: but that's like saying "AI is hard"
aCleverEpithet: thats a good point actually
GusLacerda: I am happy to make incremental progress
GusLacerda: record people doing it
GusLacerda: figure out how they're doing it
GusLacerda: formalize it
GusLacerda: and implement it
GusLacerda: that's it!
GusLacerda: of course, this only works for reasoning-based tasks
GusLacerda: you can't necessarily figure out what people are doing if it involves unconscious pattern-recognition
aCleverEpithet: yes, i wonder how much that actually comes into play
aCleverEpithet: if it is more or less than we think
GusLacerda: hard to say
GusLacerda: certainly, a lot of the things we find hard to formalize in math, are *not* due to such processes
GusLacerda: but rather due to us not having cognitively-faithful representations
GusLacerda: like diagrammatic reasoning, which we're making progress on
GusLacerda: a lot of math and science is reasoning
aCleverEpithet: definitely
GusLacerda: formalizing it can't be bad
GusLacerda: maybe 100% of algorithm discovery is reasoning
aCleverEpithet: i can't think of any examples of algorithm discovery that are not just reasoning
GusLacerda: me neither
GusLacerda: although in some cases, spatial reasoning is needed
GusLacerda: or maybe that's just mathematical reasoning
aCleverEpithet: yeah, im not usre
aCleverEpithet: i think it's a kind of mathematical reasoning
GusLacerda: well, algorithm discovery IS mathematical discovery
...
GusLacerda: anyway, this stuff is an interesting mix of theoretical and empirical reasoning
[...just like scientific discovery and ordinary mathematical discovery]