5 ms·

> C99 and C11 are great languages. I think the amount of undefined behavior in C--and that undefined behavior is necessary to compensate for its design mistake

> C99 and C11 are great languages. I think the amount of undefined behavior in C--and that undefined behavior is necessary to compensate for its design mistakes (e.g. signed overflow)--disqualifies it from being a "great language". Empirically, virtually every single large C program in existence depends on undefined behavior to continue working. And that UB is very difficult to spot [1]. > It'd be nice to be able to define how memory should be handled for a particular application at the granularity of the target platform while still getting the safety guarantees. > I like where Blow is going with his Jai language. It'd be neat to see more research in this area. You said that you wanted safety guarantees, but Jai is explicitly not about safety guarantees. In fact, being memory unsafe is one of the key design criteria behind the language. That's what differentiates it from for example Rust. [1]: https://news.ycombinator.com/item?id=11728324 https://news.ycombinator.com/item?id=11728324

agentultra 10y ago
I don't disagree wrt. UB. I've read somewhere that the reason C is so portable, despite not being designed that way, might be due to "underspecification." Regardless it's something one must be aware of. As for Jai, etc... right. I was conflating two things. Jai for keeping the spirit of C wrt "the programmer is in control." The other idea being FP languages with hardware-level capabilities.
- catnaroek 10y ago
  > The other idea being FP languages with hardware-level capabilities. This won't happen until FP implementors work on bridging the gap between typed lambda calculi (ideal source languages) and the C machine model (ideal target machine). This needs: (0) A limited form of dependent types, tailored to express invariants of data structures, rather than arbitrary mathematical propositions. (1) Substructural types, so that use-once objects can be reclaimed eagerly and deterministically. (2) Designing abstractions so that their implementations have no overhead with respect to what a C programmer could have done manually. But FP people in general don't seem terribly interested in any of these. Instead they write compilers targeting JavaScript.
  - agentultra 10y ago
    With my limited experience in Agda I'm really excited about dependent types. I've been under the impression that there is some research in this area...
    - catnaroek 10y ago
      A language whose type level allows you to express arbitrary mathematical propositions can't possibly have as good inference as ML and Haskell have, because higher-order unification is known to be undecidable. Agda and Idris require manual type annotations for all let-bound identifiers. Coq requires all dependent pattern-matching blocks to be type-annotated. This is a real chore, and dependent types will never become mainstream unless their usability improves significantly. What I have in mind is one way to hopefully achieve that “significant usability improvement”: (0) Have dependent types, but restrict them to be first-order. This is good enough for programming purposes: invariants of data structures can almost always be expressed as first-order formulas. (1) Use known and proven type inference technology: generate a system of type-level equations, and solve them via first-order unification, which is known to be decidable and tractable in practice. But I don't see anyone in the FP community exploring this possibility.
      - nickpsecurity 10y ago
        I just got a bunch of papers on first-order verification, implementation, compilers, and so on as the simplicity & tractability part peaked my interest. I'm keeping them in case I run into some students or hobbyists that want to try that on top of some "verify the verifier" kind of issues. Then I see these suggestions... "(0) Have dependent types, but restrict them to be first-order. This is good enough for programming purposes: invariants of data structures can almost always be expressed as first-order formulas. (1) Use known and proven type inference technology: generate a system of type-level equations, and solve them via first-order unification, which is known to be decidable and tractable in practice." I'll add those to the list given that sounds worth a good try. Especially if combined with automated approaches to generating & solving for common attributes like in SPARK and AutoCorres. Maybe something will come of it.
vonmoltke 10y ago
> I think the amount of undefined behavior in C--and that undefined behavior is necessary to compensate for its design mistakes (e.g. signed overflow)--disqualifies it from being a "great language". The undefined behavior is there primarily to account for the variation in platforms. Higher-level languages avoid this by hiding it in a platform-specific compiler or VM, which in turn limits the number of platforms the code can actually be run on. > Empirically, virtually every single large C program in existence depends on undefined behavior to continue working. Citation needed. I get that undefined behavior is hard to spot, but having spent years writing cross-platform C I cannot accept that every large program depends on it without some evidence.
- catnaroek 10y ago
  > The undefined behavior is there primarily to account for the variation in platforms. Honest question: Doesn't implementation-defined behavior suffice to address variations across platforms? Undefined behavior has far more drastic consequences: compilers are allowed to assume it simply won't happen.
  - vonmoltke 10y ago
    On further review, I think I was conflating undefined behavior with implementation-defined behavior. As pcwalton pointed out, though, in the early days there wasn't really a distinction between the two.
- pcwalton 10y ago
  > The undefined behavior is there primarily to account for the variation in platforms. Higher-level languages avoid this by hiding it in a platform-specific compiler or VM, which in turn limits the number of platforms the code can actually be run on. It may have started this way in the committee (though that isn't true for e.g. type based alias rules), but nowadays it's depended on for performance. You lose a lot of ability to reason about loop trip count if signed overflow is defined, for example. > Citation needed. I get that undefined behavior is hard to spot, but having spent years writing cross-platform C I cannot accept that every large program depends on it without some evidence. The probability that a program depends on any of (nonexhaustive list) (a) inspecting the value of a dangling pointer; (b) taking the offset from NULL; (c) type-punning through a union; (d) type-punning through any type other than char; (e) signed overflow; (f) order of operations between sequence points quickly approaches 1. Here's a very interesting survey investigating this: https://www.cl.cam.ac.uk/~pes20/cerberus/notes50-survey-discussion.html https://www.cl.cam.ac.uk/~pes20/cerberus/notes50-survey-disc...

agentultra 10y ago

I don't disagree wrt. UB. I've read somewhere that the reason C is so portable, despite not being designed that way, might be due to "underspecification." Regardless it's something one must be aware of. As for Jai, etc... right. I was conflating two things. Jai for keeping the spirit of C wrt "the programmer is in control." The other idea being FP languages with hardware-level capabilities.

catnaroek 10y ago
> The other idea being FP languages with hardware-level capabilities. This won't happen until FP implementors work on bridging the gap between typed lambda calculi (ideal source languages) and the C machine model (ideal target machine). This needs: (0) A limited form of dependent types, tailored to express invariants of data structures, rather than arbitrary mathematical propositions. (1) Substructural types, so that use-once objects can be reclaimed eagerly and deterministically. (2) Designing abstractions so that their implementations have no overhead with respect to what a C programmer could have done manually. But FP people in general don't seem terribly interested in any of these. Instead they write compilers targeting JavaScript.
- agentultra 10y ago
  With my limited experience in Agda I'm really excited about dependent types. I've been under the impression that there is some research in this area...
  - catnaroek 10y ago
    A language whose type level allows you to express arbitrary mathematical propositions can't possibly have as good inference as ML and Haskell have, because higher-order unification is known to be undecidable. Agda and Idris require manual type annotations for all let-bound identifiers. Coq requires all dependent pattern-matching blocks to be type-annotated. This is a real chore, and dependent types will never become mainstream unless their usability improves significantly. What I have in mind is one way to hopefully achieve that “significant usability improvement”: (0) Have dependent types, but restrict them to be first-order. This is good enough for programming purposes: invariants of data structures can almost always be expressed as first-order formulas. (1) Use known and proven type inference technology: generate a system of type-level equations, and solve them via first-order unification, which is known to be decidable and tractable in practice. But I don't see anyone in the FP community exploring this possibility.
    - nickpsecurity 10y ago
      I just got a bunch of papers on first-order verification, implementation, compilers, and so on as the simplicity & tractability part peaked my interest. I'm keeping them in case I run into some students or hobbyists that want to try that on top of some "verify the verifier" kind of issues. Then I see these suggestions... "(0) Have dependent types, but restrict them to be first-order. This is good enough for programming purposes: invariants of data structures can almost always be expressed as first-order formulas. (1) Use known and proven type inference technology: generate a system of type-level equations, and solve them via first-order unification, which is known to be decidable and tractable in practice." I'll add those to the list given that sounds worth a good try. Especially if combined with automated approaches to generating & solving for common attributes like in SPARK and AutoCorres. Maybe something will come of it.

vonmoltke 10y ago

> I think the amount of undefined behavior in C--and that undefined behavior is necessary to compensate for its design mistakes (e.g. signed overflow)--disqualifies it from being a "great language". The undefined behavior is there primarily to account for the variation in platforms. Higher-level languages avoid this by hiding it in a platform-specific compiler or VM, which in turn limits the number of platforms the code can actually be run on. > Empirically, virtually every single large C program in existence depends on undefined behavior to continue working. Citation needed. I get that undefined behavior is hard to spot, but having spent years writing cross-platform C I cannot accept that every large program depends on it without some evidence.

catnaroek 10y ago
> The undefined behavior is there primarily to account for the variation in platforms. Honest question: Doesn't implementation-defined behavior suffice to address variations across platforms? Undefined behavior has far more drastic consequences: compilers are allowed to assume it simply won't happen.
- vonmoltke 10y ago
  On further review, I think I was conflating undefined behavior with implementation-defined behavior. As pcwalton pointed out, though, in the early days there wasn't really a distinction between the two.
pcwalton 10y ago
> The undefined behavior is there primarily to account for the variation in platforms. Higher-level languages avoid this by hiding it in a platform-specific compiler or VM, which in turn limits the number of platforms the code can actually be run on. It may have started this way in the committee (though that isn't true for e.g. type based alias rules), but nowadays it's depended on for performance. You lose a lot of ability to reason about loop trip count if signed overflow is defined, for example. > Citation needed. I get that undefined behavior is hard to spot, but having spent years writing cross-platform C I cannot accept that every large program depends on it without some evidence. The probability that a program depends on any of (nonexhaustive list) (a) inspecting the value of a dangling pointer; (b) taking the offset from NULL; (c) type-punning through a union; (d) type-punning through any type other than char; (e) signed overflow; (f) order of operations between sequence points quickly approaches 1. Here's a very interesting survey investigating this: https://www.cl.cam.ac.uk/~pes20/cerberus/notes50-survey-discussion.html https://www.cl.cam.ac.uk/~pes20/cerberus/notes50-survey-disc...