4 ms·

Great list for inspiration! Though, it is not true that all the problems can be solved in any programming language: try to make a "Bandwidth Monitor" in Coq.

twic 9y ago
Coq's not really a programming language, is it? It's a proof language. So, you could prove the correctness, or perhaps possibility, of a bandwidth monitor in Coq, given certain assumptions, but it would be up to some other poor schmuck to actually write it.
- madsbuch 9y ago
  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:
brians 9y ago
I think that looks like a framework for proving things about the bandwidth usage of other programs, no?
- madsbuch 9y ago
  You are right :-) But we could also consider another example: try to return the nth digit using a regular expression.
flavio81 9y ago
+1 Or try to make an <insert non-trivial application> in Brainf*uck.

twic 9y ago

Coq's not really a programming language, is it? It's a proof language. So, you could prove the correctness, or perhaps possibility, of a bandwidth monitor in Coq, given certain assumptions, but it would be up to some other poor schmuck to actually write it.

madsbuch 9y ago
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:

brians 9y ago

I think that looks like a framework for proving things about the bandwidth usage of other programs, no?

madsbuch 9y ago
You are right :-) But we could also consider another example: try to return the nth digit using a regular expression.

flavio81 9y ago

+1 Or try to make an <insert non-trivial application> in Brainf*uck.