6 ms·

My language works a little like this. All programs are verified to be safe (not crash, read out of bounds, etc), and to terminate.

al2o3cr 12y ago
"and to terminate" That must be a neat trick - or you've constructed a non-Turing -complete language...
- skew 12y ago
  Non-Turing-complete is not a bad way to go. You pretty much have to already be a researcher in dependent type systems (or maybe set theory) to invent functions that always terminate but can't be written in non-Turing-complete languages like Coq (an evaluator for programs in an at-least-as-powerful dependently typed language is the only remotely natural example I know of). Also, writing a program that proves some programs terminate is way easier than proving a program that correctly proves any terminating program terminates, if you are confusing the two. If it's not too common, "I didn't manage to prove this terminates" sounds like a reasonable compiler error.
  - tel 12y ago
    It can be kind of hard to satisfy termination checkers, though. They're not smart. You basically have to show structural induction on something which sometimes forces you to invent lots of new proof terms.
    - Ono-Sendai 12y ago
      Indeed. I suspect that's where a lot of my time will be invested, making the checker better, improving error messages, etc..
  - dllthomas 12y ago
    "(an evaluator for programs in an at-least-as-powerful dependently typed language is the only remotely natural example I know of)" Note, also, that there's an obvious restriction for that case to get something you can write: "evaluate for the next X steps".
- eru 12y ago
  Finding non-Turing complete, but still interesting languages, is a noble pursuit.
  - tel 12y ago
    Why? PFPL has like 10 chapters on them. It's never really been stated why Completeness is a good thing.
    - eru 12y ago
      Yes. It's a useful endeavour. Things like Datalog, regular expressions or applicative parser combinators come out of it.
- qu4z-2 12y ago
  Or it just refuses to compile/execute something it can't prove terminates.
  - TheCoelacanth 12y ago
    That would make it non-Turing complete. Of course there probably aren't many interesting programs that are ruled out by that restriction.
    - marcosdumay 12y ago
      There are many interesting programs that don't ave any guarantee that they terminate. A a few that don't really terminate, ever. In fact, if you click on the launcher menu on your computer, I'll bet most programs there just keep going, until some random event (AKA clicking on an "x") throws them out of the loop.
      - TheCoelacanth 12y ago
        It wouldn't require that all programs terminate, just that all functions terminate.
        marcosdumay 12y ago
        Your programs aren't composed of one top-level function?
        TheCoelacanth 12y ago
        More likely they would be composed on one top-level IO value, like in Haskell, or something similar.
      - eru 12y ago
        That's why you'd ask your programs to be `productive'. Also look up co-recursion and co-data, if you want to find out more about this. (It's basically the logical way to extend `termination' from batch programs to things like continuously running programs like operating systems.)
- Ono-Sendai 12y ago
  Yeah, it's non turing-complete.

al2o3cr 12y ago

"and to terminate" That must be a neat trick - or you've constructed a non-Turing -complete language...

skew 12y ago
Non-Turing-complete is not a bad way to go. You pretty much have to already be a researcher in dependent type systems (or maybe set theory) to invent functions that always terminate but can't be written in non-Turing-complete languages like Coq (an evaluator for programs in an at-least-as-powerful dependently typed language is the only remotely natural example I know of). Also, writing a program that proves some programs terminate is way easier than proving a program that correctly proves any terminating program terminates, if you are confusing the two. If it's not too common, "I didn't manage to prove this terminates" sounds like a reasonable compiler error.
- tel 12y ago
  It can be kind of hard to satisfy termination checkers, though. They're not smart. You basically have to show structural induction on something which sometimes forces you to invent lots of new proof terms.
  - Ono-Sendai 12y ago
    Indeed. I suspect that's where a lot of my time will be invested, making the checker better, improving error messages, etc..
- dllthomas 12y ago
  "(an evaluator for programs in an at-least-as-powerful dependently typed language is the only remotely natural example I know of)" Note, also, that there's an obvious restriction for that case to get something you can write: "evaluate for the next X steps".
eru 12y ago
Finding non-Turing complete, but still interesting languages, is a noble pursuit.
- tel 12y ago
  Why? PFPL has like 10 chapters on them. It's never really been stated why Completeness is a good thing.
  - eru 12y ago
    Yes. It's a useful endeavour. Things like Datalog, regular expressions or applicative parser combinators come out of it.
qu4z-2 12y ago
Or it just refuses to compile/execute something it can't prove terminates.
- TheCoelacanth 12y ago
  That would make it non-Turing complete. Of course there probably aren't many interesting programs that are ruled out by that restriction.
  - marcosdumay 12y ago
    There are many interesting programs that don't ave any guarantee that they terminate. A a few that don't really terminate, ever. In fact, if you click on the launcher menu on your computer, I'll bet most programs there just keep going, until some random event (AKA clicking on an "x") throws them out of the loop.
    - TheCoelacanth 12y ago
      It wouldn't require that all programs terminate, just that all functions terminate.
      - marcosdumay 12y ago
        Your programs aren't composed of one top-level function?
        TheCoelacanth 12y ago
        More likely they would be composed on one top-level IO value, like in Haskell, or something similar.
    - eru 12y ago
      That's why you'd ask your programs to be `productive'. Also look up co-recursion and co-data, if you want to find out more about this. (It's basically the logical way to extend `termination' from batch programs to things like continuously running programs like operating systems.)
Ono-Sendai 12y ago
Yeah, it's non turing-complete.