8 ms·

Decidability. :) I'd love to see that show up in more languages. I believe it allows for better abstractions without optimization deficiencies because it's all

Decidability. :) I'd love to see that show up in more languages. I believe it allows for better abstractions without optimization deficiencies because it's all decidable.

simcop2387 9y ago
The big problem with that is that if a language is decidable it can't be Turing complete. That means that a large number of useful programs are just not going to be expressible. That said for something g like this it's a perfect fit to have it be decidable.
- chowells 9y ago
  There are no useful programs that require Turing completeness. That's basically by definition. Turing completeness is what allows programs to have non-productive infinite loops. Any system that guarantees productivity isn't Turing complete. All useful algorithms are productive. The only thing you can do with a non-productive algorithm is convert electricity to heat.
  - saghm 9y ago
    I took a course in college where we used Coq to build up an imperative programming language, and I waa surprised how much you could do (i.e. essentially anything you needed to) with a non-Turing complete language. I think that the traditional computer science curriculum makes such a big deal about Turing machines (and not necessarily wrongly so) that students just assume that Turning completeness is a natural goal to strive for rather than just a property with tradeoffs, just like any other property. It certainly doesn't help that it seems harder to create a language that's not Turing complete than one that is, at least if you aren't explicitly trying to avoid it; just look at all the random things that have been discovered to be accidentally Turing complete over the years.
  - deleted 9y ago
    [deleted]
  - avaer 9y ago
    Doesn't any program that processes interactive/network IO require an infinite loop? Are those programs not useful?
    - eberkund 9y ago
      No, they can use interrupts instead.
      - avaer 9y ago
        I don't understand how that avoids looping. If your program doesn't loop waiting for interrupts, it has terminated. So it won't be getting those interrupts.
    - dragonwriter 9y ago
      > Doesn't any program that processes interactive/network IO require an infinite loop? No. I mean, there are lots of common uses of unbounded loops in that domain, but any of them could be replaced with maximum-bounded loops with sufficient large bounds and be unnoticeably different in practice, mostly cutting off (largely pathological) edge cases.
      - mbrock 9y ago
        It seems that a better solution is to guarantee that each step of such an unbounded loop is bounded, and clearly distinguish these types of processes. For example, a kernel's scheduler should run indefinitely, but each scheduling step should be bounded. Ideally we would specify the scheduler loop as a non-terminating yet "productive" process.
  - simcop2387 9y ago
    So I might have made this a bit confusing too by conflating the two things in my original post. The real thing is that there are a lot of undecidable programs that don't require Turing completeness. And a lot of those useful programs are undecidable, an example of a really simple undecidable program: 10 PRINT "Enter your name" 20 INPUT NAME$ 30 PRINT "Hello ", NAME$ 40 IF NAME$ <> "Ralph" THEN 41 GOTO 10 42 END IF 50 PRINT "Goodby Ralph" That program, because it might loop indefinitely isn't decidable and isn't possible to describe with Viper by design. This kind of program is pretty analogous to basically every program that communicates with the network, user, or some other external system.
    - dragonwriter 9y ago
      > This kind of program is pretty analogous to basically every program that communicates with the network, user, or some other external system. Not really; it's quite possible, and often desirable, to do that without potentially infinite loops.
      - sillysaurus3 9y ago
        How?
      - swsieber 9y ago
        Exactly - you want timeouts, exponential backoff, etc. You want to know what happens if a network failure happens - you don't want to retry ad nauseam.
        sillysaurus3 9y ago
        Some of the most reliable programs are those without exponential backoff and which retry infinitely in network failure situations. `ping` is one example.
        swsieber 9y ago
        And yet I'd be completely fine with a ping that was capped to running for no more than a week. YMMV though. And more to the point, you don't want a program that goes on forever in a setup like ethereum. I guess your rebuttal was called for since the initial point was a little hyperbolic.
  - TelmoMenezes 9y ago
    > Any system that guarantees productivity isn't Turing complete. All useful algorithms are productive. But it does not follow that all useful algorithms can be implemented on a language that "guarantees productivity". Turing proved that the halting problem cannot be solved on a Turing machine. This opens the possibility for the existence of programs that might be "productive" in your sense, but might also never stop, and it is not possible to know in advance. > The only thing you can do with a non-productive algorithm is convert electricity to heat. I am not convinced of this at all. Perhaps true if you are talking about banking systems or web applications, but probably not true if you are talking about AI. Intermediary states of an endless computation might be interesting. Maybe this is a way to obtain unbounded creativity. Maybe this is the way to build minds. We don't know enough. A more general observation: I find that we live in an era that is too obsessed with productivity at the cost of fundamental research, dreaming and imagination. I am convinced that the latter mindset is the only one that can bring qualitative changes to our culture and civilisation, and I think that our long-term survival depends on such qualitative jumps. Of course, I also understand that someone has to take care of the plumbing...
    - lmm 9y ago
      > Turing proved that the halting problem cannot be solved on a Turing machine. This opens the possibility for the existence of programs that might be "productive" in your sense, but might also never stop, and it is not possible to know in advance. Maybe. I struggle to imagine a practical case where we want to run a program that we didn't and couldn't know whether it worked though. > I am not convinced of this at all. Perhaps true if you are talking about banking systems or web applications, but probably not true if you are talking about AI. Intermediary states of an endless computation might be interesting. Maybe this is a way to obtain unbounded creativity. Maybe this is the way to build minds. We don't know enough. This is ridiculous reasoning. "We don't understand X, we don't understand Y, therefore X might be related to Y." > A more general observation: I find that we live in an era that is too obsessed with productivity at the cost of fundamental research, dreaming and imagination. I am convinced that the latter mindset is the only one that can bring qualitative changes to our culture and civilisation, and I think that our long-term survival depends on such qualitative jumps. > Of course, I also understand that someone has to take care of the plumbing... Choosing to look at non-halting programs rather than halting programs is like choosing to look at crystal energy instead of nuclear fusion. A certain amount of willingness to question baseline assumptions is valuable, but I think our long-term survival depends far more on being willing to acknowledge the fundamental results of the field and put in the hard engineering work necessary to achieve things under the constraints of reality, rather than trying to wave them away.
  - dnautics 9y ago
    > All useful algorithms are productive. I'm gonna have to call "not quite" on that one. There's some zeroth-order truth and appeal to that statement, but there are certainly stochastic algorithms that have virtually guaranteed to be awesome, but have a nonzero likelihood, unbounded worst case scenario.
- deleted 9y ago
  [deleted]
- dom0 9y ago
  AIUI smart contracts mean that a ton of nodes has to execute this code, so making the language of the code as weak as possible would seem like an important design goal to me from a langsec PoV.
tom_mellior 9y ago
Decidability doesn't necessarily imply the absence of "optimization deficiencies". Many program analyses make approximations not (only) because of undecidability but simply due to complexity issues. Even in decidable languages it's trivial to write programs with an exponential number of code paths, which forces analyzers to make approximations.
etatoby 9y ago
Is there any practical programming language (or dialect, or static checker) that enforces this property? Or is Viper the first attempt at a usable, yet decidable language?
- tom_mellior 9y ago
  I could think of some examples, but you might disagree on the "practical" part. If I recall correctly, Pascal-style languages have counting for loops where you cannot modify the loop counter or the loop bound inside the loop. That is, you must use a while or repeat loop or recursion to have non-termination. A Pascal compiler would be trivial to extend with syntactic checks for the absence of such loops and recursion. But I don't think it's been done. You could go towards more programming flexibility but a higher proof burden and use Spark/Ada (for Ada) or Frama-C (for C), but you would need to annotate loops with variant expressions to help the system prove termination. Note that if you find languages without general loops and without recursion impractical, you might be disappointed by Viper as well. According to the grammar given on GitHub, Viper only has counting loops and no function calls at all except to a few built-in functions. The latter might just be an oversight, though. Functions are too useful to get rid of completely.

Decidability. :) I'd love to see that show up in more languages. I believe it allows for better abstractions without optimization deficiencies because it's all decidable.

simcop2387 9y ago

The big problem with that is that if a language is decidable it can't be Turing complete. That means that a large number of useful programs are just not going to be expressible. That said for something g like this it's a perfect fit to have it be decidable.

chowells 9y ago
There are no useful programs that require Turing completeness. That's basically by definition. Turing completeness is what allows programs to have non-productive infinite loops. Any system that guarantees productivity isn't Turing complete. All useful algorithms are productive. The only thing you can do with a non-productive algorithm is convert electricity to heat.
- saghm 9y ago
  I took a course in college where we used Coq to build up an imperative programming language, and I waa surprised how much you could do (i.e. essentially anything you needed to) with a non-Turing complete language. I think that the traditional computer science curriculum makes such a big deal about Turing machines (and not necessarily wrongly so) that students just assume that Turning completeness is a natural goal to strive for rather than just a property with tradeoffs, just like any other property. It certainly doesn't help that it seems harder to create a language that's not Turing complete than one that is, at least if you aren't explicitly trying to avoid it; just look at all the random things that have been discovered to be accidentally Turing complete over the years.
- deleted 9y ago
  [deleted]
- avaer 9y ago
  Doesn't any program that processes interactive/network IO require an infinite loop? Are those programs not useful?
  - eberkund 9y ago
    No, they can use interrupts instead.
    - avaer 9y ago
      I don't understand how that avoids looping. If your program doesn't loop waiting for interrupts, it has terminated. So it won't be getting those interrupts.
  - dragonwriter 9y ago
    > Doesn't any program that processes interactive/network IO require an infinite loop? No. I mean, there are lots of common uses of unbounded loops in that domain, but any of them could be replaced with maximum-bounded loops with sufficient large bounds and be unnoticeably different in practice, mostly cutting off (largely pathological) edge cases.
    - mbrock 9y ago
      It seems that a better solution is to guarantee that each step of such an unbounded loop is bounded, and clearly distinguish these types of processes. For example, a kernel's scheduler should run indefinitely, but each scheduling step should be bounded. Ideally we would specify the scheduler loop as a non-terminating yet "productive" process.
- simcop2387 9y ago
  So I might have made this a bit confusing too by conflating the two things in my original post. The real thing is that there are a lot of undecidable programs that don't require Turing completeness. And a lot of those useful programs are undecidable, an example of a really simple undecidable program: 10 PRINT "Enter your name" 20 INPUT NAME$ 30 PRINT "Hello ", NAME$ 40 IF NAME$ <> "Ralph" THEN 41 GOTO 10 42 END IF 50 PRINT "Goodby Ralph" That program, because it might loop indefinitely isn't decidable and isn't possible to describe with Viper by design. This kind of program is pretty analogous to basically every program that communicates with the network, user, or some other external system.
  - dragonwriter 9y ago
    > This kind of program is pretty analogous to basically every program that communicates with the network, user, or some other external system. Not really; it's quite possible, and often desirable, to do that without potentially infinite loops.
    - sillysaurus3 9y ago
      How?
    - swsieber 9y ago
      Exactly - you want timeouts, exponential backoff, etc. You want to know what happens if a network failure happens - you don't want to retry ad nauseam.
      - sillysaurus3 9y ago
        Some of the most reliable programs are those without exponential backoff and which retry infinitely in network failure situations. `ping` is one example.
        swsieber 9y ago
        And yet I'd be completely fine with a ping that was capped to running for no more than a week. YMMV though. And more to the point, you don't want a program that goes on forever in a setup like ethereum. I guess your rebuttal was called for since the initial point was a little hyperbolic.
- TelmoMenezes 9y ago
  > Any system that guarantees productivity isn't Turing complete. All useful algorithms are productive. But it does not follow that all useful algorithms can be implemented on a language that "guarantees productivity". Turing proved that the halting problem cannot be solved on a Turing machine. This opens the possibility for the existence of programs that might be "productive" in your sense, but might also never stop, and it is not possible to know in advance. > The only thing you can do with a non-productive algorithm is convert electricity to heat. I am not convinced of this at all. Perhaps true if you are talking about banking systems or web applications, but probably not true if you are talking about AI. Intermediary states of an endless computation might be interesting. Maybe this is a way to obtain unbounded creativity. Maybe this is the way to build minds. We don't know enough. A more general observation: I find that we live in an era that is too obsessed with productivity at the cost of fundamental research, dreaming and imagination. I am convinced that the latter mindset is the only one that can bring qualitative changes to our culture and civilisation, and I think that our long-term survival depends on such qualitative jumps. Of course, I also understand that someone has to take care of the plumbing...
  - lmm 9y ago
    > Turing proved that the halting problem cannot be solved on a Turing machine. This opens the possibility for the existence of programs that might be "productive" in your sense, but might also never stop, and it is not possible to know in advance. Maybe. I struggle to imagine a practical case where we want to run a program that we didn't and couldn't know whether it worked though. > I am not convinced of this at all. Perhaps true if you are talking about banking systems or web applications, but probably not true if you are talking about AI. Intermediary states of an endless computation might be interesting. Maybe this is a way to obtain unbounded creativity. Maybe this is the way to build minds. We don't know enough. This is ridiculous reasoning. "We don't understand X, we don't understand Y, therefore X might be related to Y." > A more general observation: I find that we live in an era that is too obsessed with productivity at the cost of fundamental research, dreaming and imagination. I am convinced that the latter mindset is the only one that can bring qualitative changes to our culture and civilisation, and I think that our long-term survival depends on such qualitative jumps. > Of course, I also understand that someone has to take care of the plumbing... Choosing to look at non-halting programs rather than halting programs is like choosing to look at crystal energy instead of nuclear fusion. A certain amount of willingness to question baseline assumptions is valuable, but I think our long-term survival depends far more on being willing to acknowledge the fundamental results of the field and put in the hard engineering work necessary to achieve things under the constraints of reality, rather than trying to wave them away.
- dnautics 9y ago
  > All useful algorithms are productive. I'm gonna have to call "not quite" on that one. There's some zeroth-order truth and appeal to that statement, but there are certainly stochastic algorithms that have virtually guaranteed to be awesome, but have a nonzero likelihood, unbounded worst case scenario.
deleted 9y ago
[deleted]
dom0 9y ago
AIUI smart contracts mean that a ton of nodes has to execute this code, so making the language of the code as weak as possible would seem like an important design goal to me from a langsec PoV.

tom_mellior 9y ago

Decidability doesn't necessarily imply the absence of "optimization deficiencies". Many program analyses make approximations not (only) because of undecidability but simply due to complexity issues. Even in decidable languages it's trivial to write programs with an exponential number of code paths, which forces analyzers to make approximations.

etatoby 9y ago

Is there any practical programming language (or dialect, or static checker) that enforces this property? Or is Viper the first attempt at a usable, yet decidable language?

tom_mellior 9y ago
I could think of some examples, but you might disagree on the "practical" part. If I recall correctly, Pascal-style languages have counting for loops where you cannot modify the loop counter or the loop bound inside the loop. That is, you must use a while or repeat loop or recursion to have non-termination. A Pascal compiler would be trivial to extend with syntactic checks for the absence of such loops and recursion. But I don't think it's been done. You could go towards more programming flexibility but a higher proof burden and use Spark/Ada (for Ada) or Frama-C (for C), but you would need to annotate loops with variant expressions to help the system prove termination. Note that if you find languages without general loops and without recursion impractical, you might be disappointed by Viper as well. According to the grammar given on GitHub, Viper only has counting loops and no function calls at all except to a few built-in functions. The latter might just be an oversight, though. Functions are too useful to get rid of completely.