7 ms·

...you'd have to write it in C (or something equivalently dangerous), because you can't prove big runtimes... In order for this argument to hold, we would have

• marcosdumay 10y ago
  Wait, is there a high level language (not assembly) with no runtime out there? I don't think we are talking about the same thing at all.
  • steveklabnik 10y ago
    They're making an oblique reference to Rust; it has the same level of runtime that C does. Many people say "no runtime" to mean "small runtime like C or C++ have" rather than literally no runtime. This is due to the confusion around interpreters sometimes being called "runtimes."
    • marcosdumay 10y ago
      I suspect it was something about compiled vs. interpreted. The Rust runtime is larger than C's (I imagine it's not much larger than C++, but this is already way too large). AFAIK, nobody ever proved it works as designed. The fact that it's design is not very stable is also a problem. Now, with some more thought about it, C itself is not a great target for correctness proofs. Too much is left unspecified, and there is little agreement over some of the lower level stuff. A simplified version of Rust might be a better target than C, if somebody ever creates it, but a lot of the safety would have to be left out of it.
      • Manishearth 10y ago
        IIRC Rust by default brings in a few things (panic handling is the main one, and also jemalloc) that make its runtime larger than C (but not larger than C++), but they can be disabled with compile flags. Many folks do, for embedded stuff. Rust also lets you write a custom runtime by specifying a start function if you want. > The fact that it's design is not very stable is also a problem. Rust is stable.
      • steveklabnik 10y ago
        > The Rust runtime is larger than C's (I imagine it's not much larger than C++, but this is already way too large). I believe that it is smaller than C++'s but larger than C's, but I'm not a mega expert here. I used to know where those files were located in-tree, but don't anymore. I think there's also several distinctions you can draw here; for example, strictly speaking, almost no runtime is required, but if you're using say, the standard library, you still might end up with a bunch of code. The actual requirements are very small though. > AFAIK, nobody ever proved it works as designed. The fact that it's design is not very stable is also a problem. Sorry, I don't understand what you mean here. The runtime? > A simplified version of Rust might be a better target than C, if somebody ever creates it, but a lot of the safety would have to be left out of it. I _think_ with the above comments, you mean the Rust langauge overall, not the runtime, right? So, Rust _is_ very stable; post 1.0 we have made extremely small breaking changes, corresponding to the way new C++ standards sometimes introduce minor technical backwards incompatibilities. As for correctness proofs, there are multiple academic institutions working on it; and they don't have to "leave the safety out"; that's what they're trying to prove!
        • Manishearth 10y ago
          https://github.com/rust-lang/rust/blob/1ca100d0428985f916eea153886762bed3909771/src/libstd/rt.rs#L31-L67 https://github.com/rust-lang/rust/blob/1ca100d0428985f916eea... is the "runtime". sys::thread contains all the TLS stuff (C has TLS too, so it's unclear if this is any more of a runtime). catch_unwind is for toplevel panic handling (which can be nop'd with panic=abort). Finally, we link to jemalloc, which is an additional bit of runtime of its own (which can be turned off with alloc_system)
          • steveklabnik 10y ago
            Ah right, it's in src\libstd\rt.rs, not src\rt, ha!
            • Manishearth 10y ago
              It used to be! There's also compiler-rt which does some of the eh stuff for panics and whatnot.
  • pjmlp 10y ago
    Modula-2, Oberon, Ada, Turbo Pascal, Free Pascal, Object Pascal, Quick Basic, Oberon-2, Active Oberon, Oberon-07, CLU, System C#, Modula-2+, Modula-3, D, Cyclone, ATS, Mesa, Algol, PL/I, PL/M,...