Programming as interaction: A new perspective for programming language research

- Brad Myer's Natural Programming Project at CMU (tons of novel tools!): http://www.cs.cmu.edu/~NatProg/index.html

- Andy Ko's work on debugging and learning to code: http://faculty.washington.edu/ajko/publications

- Emerson Murphy-Hill's work on the usability of dev tools, especially refactoring tools: https://people.engr.ncsu.edu/ermurph3/pubs.html

- Chris Parnin's studies on the cognitive aspects of coding: http://chrisparnin.me/

- Chrsitian Bird's empirical studies of developers: http://www.cabird.com/wp/publications/

- Thomas LaToza's work on the collaborative aspects of development: https://cs.gmu.edu/~tlatoza/papers.html

- Bjorn Hartmann's help support in code editors and tutorial generation: https://people.eecs.berkeley.edu/~bjoern/

- Philip Guo's tools to support novices with coding: http://www.pgbovine.net/publications.htm

- My dissertation "Human-Centric Tools for Navigating Code": http://web.eecs.utk.edu/~azh/publications.html

- Margaret Burnett's work on how people forage for information in code: http://web.engr.oregonstate.edu/~burnett/reprints.html

First:

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.455... The Interactive Nature of Computing: Refuting the Strong Church-Turing Thesis

And related research, such as the one pointed out in this hacker news comments thread:

https://news.ycombinator.com/item?id=17292935

(Full comments for that submission, "Are real numbers really real?" here: https://news.ycombinator.com/item?id=17291752)

For more, albeit more peripherally related, see also here:

https://arxiv.org/abs/0806.3972 Short note on additive sequences and on recursive processes;

from where I'll quote:

"It seems obvious that any ‘grammar’ that would engender the words – and only the words – of the above described recursive sequence has infinitely many rules (even if we can express them all in a finite number of English words) and as such does not belong to ‘formal’ grammars. Of course, the use of these new rules at every step of the process is limited, because it depends of the steps themselves. Nevertheless, it seems that the set of the generated words is not included in the outcome vocabulary of any formal grammar. Therefore it doesn’t correspond to any Turing Machine. Inasmuch it seems to be, in some sense, calculable and recursively enumerable, one can ask: how to build an automaton able to recognize them? How about the celebrated Church-Turing Thesis and the way it is understood or misunderstood?"

[

For EVEN MORE misunderstandings about Turing completeness, see also this Scala-related paper:

http://drops.dagstuhl.de/opus/volltexte/2017/7276/pdf/LIPIcs...

Which points out that one can do certain forms of recursion, specifically, https://en.wikipedia.org/wiki/Bounded_quantification#F-bound..., via recursive self-types, without turing completeness.

]