|
|
|
|
|
|
by tpetricek
2807 days ago
|
|
|
Author here. I'm aware of work in this area (though certainly not all of it) and I had the pleasure of attending last two PPIGs! The idea I outlined in the blog post is absolutely inspired by all of this, but I think there is one fundamental difference (which perhaps is not as clearly explained as it should have been). People in the HCI world study interactions that happen in programming and use that as a source of ideas for how to design languages. However, what I'm proposing is to make those "interactions" a part of the language definition. (HCI is a great source of ideas for understanding what those interactions are, but you can then study the resulting things in many ways, including formal methods - which is what I find interesting). As far as I know, the related work that actually does what I'm describing is two things already mentioned in the blog post (Subtext, Inferential Programming) and one idea someone mentioned on Twitter is Programming by Example, which I think is close too. tldr; I'm not talking about studying programming via the perspective of human computer interaction, but about making those first-class language constructs. |
|
|
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.
]