4 ms·

Well, what constitutes a programming language then? It sounds like there is a clear definition :-) Coq is certainly a programming language, as you can build pr

Well, what constitutes a programming language then? It sounds like there is a clear definition :-) Coq is certainly a programming language, as you can build programs. But you can't interact with the subsystem, you can only build pure functions (Therefore it is quite hard to build a performance monitor). In my opinion English could also go as a programming language. Especially given the rise in NLP products. You can actually program a computer to do quite advanced tasks solely through natural languages.

gerdesj 9y ago
"Well, what constitutes a programming language then? It sounds like there is a clear definition :-)" Some bloke called Turing had a few ideas on a definition. (I'll whisper "whoosh" here - for my own note) Given that any programming language can be defined in English (or any other human language, with a few contortions as required, if any) then of course English can be used to create a Turing Machine (TM). It doesn't take much NLP to define a full TM via speech.
- madsbuch 9y ago
  I am not aware of his definition? I can't find it on google either. Can you point me to it? A Turing machine does not talk about expressing computations, but rather a class of problems that can be computed. Remember, not all programming languages are Turing complete (Coq being one of them).
  - gerdesj 9y ago
    I can still hear "whoosh" in my own ears here 8) Given how simple a Turing Machine can be, I seriously doubt (without any proof) that coq is not able to recreate a TM. I am not an expert but the explanation about Turing Machines I read was in GED and involved a simple tape and a slack handful of symbols and operations and some basic hand waving. If coq can't manage that then it is unlikely to be useful - which I doubt.
    - madsbuch 9y ago
      You should check you ears. Coq only accepts well funded recursion. Non-bound Turing machines span a bigger complexity class. In other words: Turing machines can loop forever, Coq can not express programs that can do so. Read your CS 101:

gerdesj 9y ago

"Well, what constitutes a programming language then? It sounds like there is a clear definition :-)" Some bloke called Turing had a few ideas on a definition. (I'll whisper "whoosh" here - for my own note) Given that any programming language can be defined in English (or any other human language, with a few contortions as required, if any) then of course English can be used to create a Turing Machine (TM). It doesn't take much NLP to define a full TM via speech.

madsbuch 9y ago
I am not aware of his definition? I can't find it on google either. Can you point me to it? A Turing machine does not talk about expressing computations, but rather a class of problems that can be computed. Remember, not all programming languages are Turing complete (Coq being one of them).
- gerdesj 9y ago
  I can still hear "whoosh" in my own ears here 8) Given how simple a Turing Machine can be, I seriously doubt (without any proof) that coq is not able to recreate a TM. I am not an expert but the explanation about Turing Machines I read was in GED and involved a simple tape and a slack handful of symbols and operations and some basic hand waving. If coq can't manage that then it is unlikely to be useful - which I doubt.
  - madsbuch 9y ago
    You should check you ears. Coq only accepts well funded recursion. Non-bound Turing machines span a bigger complexity class. In other words: Turing machines can loop forever, Coq can not express programs that can do so. Read your CS 101: