3 ms·

Duly upvoted, but I'd like to note that the problem with so-called “unsafe languages” isn't undefined behavior per se, but rather the lack of appropriate tools

Duly upvoted, but I'd like to note that the problem with so-called “unsafe languages” isn't undefined behavior per se, but rather the lack of appropriate tools (e.g. a formal axiomatic semantics) to reliably write programs with no undefined behavior.

solidsnack9000 10y ago
As long as you use the new semantics, the unsafe parts of the language are barred to you, so it's like a different language.
- catnaroek 10y ago
  I'm not talking about changing languages, but rather about giving existing languages more rigorous specifications. My beef with C, C++, unsafe Rust, etc. isn't the presence of undefined behavior in arbitrary programs (for which the solution is very simple: don't write arbitrary programs!), but rather the absence of a calculational method [0] for designing programs that don't have undefined behavior (for which a formal semantics is an indispensable prerequisite). To convince yourself that a C program doesn't have undefined behavior, you need to interpret the English text of the C standard, and that's what I object to. [0] The calculations needn't be performed by a machine. If they are performed by a machine, you have a safe language. If they must be performed by humans, you have an unsafe language, which is nevertheless a lot more usable than C and friends.
  - Gankro 10y ago
    fwiw this appears to be a goal of people working on speccing out Unsafe Rust stuff. You also don't need to worry about interpreting any english specs today, because there just aren't any specs at all yet!
    - catnaroek 10y ago
      I'd have to interpret the Rustonomicon, which is still written in English. :-p
  - beached_whale 10y ago
    One can use clang and gcc to either produce a runtime error if undefined behaviour is detected or that and abort the program. There are several things, like signed overflow of integrals, that cannot often be determined at compile time.
    - johncolanduoni 10y ago
      I think the OP is referring to full-blown verification systems, like some dependently typed languages have (although they aren't the only ones). If your program's behavior is defined because you wrote it that way (i.e. not by chance), you would have an argument for why the undefined behavior is not invoked that could be translated into a formal proof in most sophisticated (i.e. ZFC-ish) formal systems.
      - catnaroek 10y ago
        Formal verification, yes. Mechanical verification (dependent types, SAT/SMT solvers, model checkers, etc.), not necessarily. I don't mean to insult the efforts of the mechanical verification community, but it's preposterous to suggest that the only way to verify programs is to use a computer. Hey, we have brains! We can use them too!
    - adrianN 10y ago
      To my knowledge the undefined behavior sanitizers are not complete. It is also unclear how you both optimize your program (exploiting undefined behavior semantics) and providing a runtime check without completely killing performance.
      - beached_whale 10y ago
        Use it during your unit tests, clang claims the runtime cost is small so it might now matter either.
    - catnaroek 10y ago
      As useful as debugging tools are, they are no replacement for design tools.
  - gsg 10y ago
    There are some tools aimed roughly in this direction, such as https://github.com/TrustInSoft/tis-interpreter https://github.com/TrustInSoft/tis-interpreter. A major difficulty here is that undefined behaviour is a property of a particular execution of a C program, rather than a static property of the program itself. Tools that dynamically detect UB are useful, but will not demonstrate that there are no inputs for which a program will go wrong.
    - catnaroek 10y ago
      As powerful as an interpreter might be for running programs, it isn't the right tool for designing programs. Validating a program design requires static analysis, to be performed either mechanically (e.g., type checking) or manually (e.g., manipulating predicate transformers in the way advocated by Dijkstra).
  - solidsnack9000 10y ago
    If you take JS and add Flow, or Python and add MyPy, and then accept the judgment of the checker and don't use the parts it doesn't check, then it becomes a language subset -- and sort of a different language. Like if you have array bounds annotations and check all indexing operations, C arrays become Pascal arrays.
    - catnaroek 10y ago
      That's the thing - I'm not talking about using any mechanical checkers. I'm talking about using a language definition that makes it easier for humans to prove things about their programs.
      - solidsnack9000 10y ago
        Okay, that's interesting. How would that work in practice? It doesn't seem like it would be easy to apply in a timely way. If the rules can be unambiguously checked by humans, would they not be more efficiently checked by machines?
        catnaroek 10y ago
        Proving theorems isn't just performing routine checks. There are creative aspects, like finding the right loop invariants, at which machines fare absolutely miserably. OTOH, machines excel at exhaustive enumeration and enforcing separation of concerns: that's why ML-style algebraic data types, pattern matching and parametric polymorphism are such a boon for high-level programming. So there's room for both human and machine work in program verification. What we should be interested in is finding the right division of labor between humans and machines.

solidsnack9000 10y ago

As long as you use the new semantics, the unsafe parts of the language are barred to you, so it's like a different language.

catnaroek 10y ago
I'm not talking about changing languages, but rather about giving existing languages more rigorous specifications. My beef with C, C++, unsafe Rust, etc. isn't the presence of undefined behavior in arbitrary programs (for which the solution is very simple: don't write arbitrary programs!), but rather the absence of a calculational method [0] for designing programs that don't have undefined behavior (for which a formal semantics is an indispensable prerequisite). To convince yourself that a C program doesn't have undefined behavior, you need to interpret the English text of the C standard, and that's what I object to. [0] The calculations needn't be performed by a machine. If they are performed by a machine, you have a safe language. If they must be performed by humans, you have an unsafe language, which is nevertheless a lot more usable than C and friends.
- Gankro 10y ago
  fwiw this appears to be a goal of people working on speccing out Unsafe Rust stuff. You also don't need to worry about interpreting any english specs today, because there just aren't any specs at all yet!
  - catnaroek 10y ago
    I'd have to interpret the Rustonomicon, which is still written in English. :-p
- beached_whale 10y ago
  One can use clang and gcc to either produce a runtime error if undefined behaviour is detected or that and abort the program. There are several things, like signed overflow of integrals, that cannot often be determined at compile time.
  - johncolanduoni 10y ago
    I think the OP is referring to full-blown verification systems, like some dependently typed languages have (although they aren't the only ones). If your program's behavior is defined because you wrote it that way (i.e. not by chance), you would have an argument for why the undefined behavior is not invoked that could be translated into a formal proof in most sophisticated (i.e. ZFC-ish) formal systems.
    - catnaroek 10y ago
      Formal verification, yes. Mechanical verification (dependent types, SAT/SMT solvers, model checkers, etc.), not necessarily. I don't mean to insult the efforts of the mechanical verification community, but it's preposterous to suggest that the only way to verify programs is to use a computer. Hey, we have brains! We can use them too!
  - adrianN 10y ago
    To my knowledge the undefined behavior sanitizers are not complete. It is also unclear how you both optimize your program (exploiting undefined behavior semantics) and providing a runtime check without completely killing performance.
    - beached_whale 10y ago
      Use it during your unit tests, clang claims the runtime cost is small so it might now matter either.
  - catnaroek 10y ago
    As useful as debugging tools are, they are no replacement for design tools.
- gsg 10y ago
  There are some tools aimed roughly in this direction, such as https://github.com/TrustInSoft/tis-interpreter https://github.com/TrustInSoft/tis-interpreter. A major difficulty here is that undefined behaviour is a property of a particular execution of a C program, rather than a static property of the program itself. Tools that dynamically detect UB are useful, but will not demonstrate that there are no inputs for which a program will go wrong.
  - catnaroek 10y ago
    As powerful as an interpreter might be for running programs, it isn't the right tool for designing programs. Validating a program design requires static analysis, to be performed either mechanically (e.g., type checking) or manually (e.g., manipulating predicate transformers in the way advocated by Dijkstra).
- solidsnack9000 10y ago
  If you take JS and add Flow, or Python and add MyPy, and then accept the judgment of the checker and don't use the parts it doesn't check, then it becomes a language subset -- and sort of a different language. Like if you have array bounds annotations and check all indexing operations, C arrays become Pascal arrays.
  - catnaroek 10y ago
    That's the thing - I'm not talking about using any mechanical checkers. I'm talking about using a language definition that makes it easier for humans to prove things about their programs.
    - solidsnack9000 10y ago
      Okay, that's interesting. How would that work in practice? It doesn't seem like it would be easy to apply in a timely way. If the rules can be unambiguously checked by humans, would they not be more efficiently checked by machines?
      - catnaroek 10y ago
        Proving theorems isn't just performing routine checks. There are creative aspects, like finding the right loop invariants, at which machines fare absolutely miserably. OTOH, machines excel at exhaustive enumeration and enforcing separation of concerns: that's why ML-style algebraic data types, pattern matching and parametric polymorphism are such a boon for high-level programming. So there's room for both human and machine work in program verification. What we should be interested in is finding the right division of labor between humans and machines.