Hacker News Reader

Comment by marcosdumay | Hacker News Reader

At extreme cases, where you want to prove your network stack, you'd have to write it in C (or something equivalently dangerous), because you can't prove big runtimes.

But in mid-way applications, dangerous languages are dangerous, and should be avoided.

I'd think the most "correct" way to handle this is to create small bits of network code with proof of correctness that handles down parsed and tagged (typed) data into code in high level languages. In that case, Curl type of code would still be in C.

View on HN

...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 to live in a world where no one has created a safe language with no runtime.

We don't live in such a world, fortunately.

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.

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."

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.

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.

> 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!

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)

Ah right, it's in src\libstd\rt.rs, not src\rt, ha!

It used to be!

There's also compiler-rt which does some of the eh stuff for panics and whatnot.

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,...

With Rust this tradeoff of safe-with-runtime vs. unsafe-without-runtime is no longer your only choice. Now you can choose safe-with-strong-compiler-no-runtime...

This tradeoff wasn't already an issue with languages like Modula and Ada.

Yeah, I realized after posting that this would be a critique. I should have stipulated that it's a C syntactic language, which seems to be many peoples preference based on the most successful languages out there.

I never did much with Ada or Modula, so I won't claim to know anything more than their syntax, etc.

As far as I am aware Ada is not memory safe without a runtime and with the presence of non-static memory. So you either have a runtime, no deallocation, or unsafety.

C also needs a runtime, it is called crt0 on UNIX and it is what calls main(), sets up global initialization functions (constructor functions in GCC C), emulates floating point,...

As for Ada, you can selectively disable which parts of the runtime actually land on the generated executable via compiler pragmas.

Deallocation can be done via pools or controlled types.

OK, I should have said garbage collector, not runtime.

Are you claiming that Module-2 is memory safe?

What about:

  MODULE Boom

  VAR Foo : POINTER TO INTEGER;

  BEGIN
    Foo^ = 123;
  END Boom.

If I remember correctly that is a compiler error, because Foo is not initialized, so no boom.

But if you still want to get your point through and have a boom.

  MODULE Boom;
  IMPORT SYSTEM;

  VAR Foo : POINTER TO INTEGER;

  BEGIN
    Foo := SYSTEM.CAST(POINTER TO INTEGER, 43414);
    Foo^ := 123;
  END Boom.

Notice the use of IMPORT SYSTEM and SYSTEM.CAST, explicit, easy to search for, and to forbid via compiler switch (no unsafe code).

Rust still has no support for true formal analysis. It is therefore pointless to use it for high safety. Use a real theorem checker instead.

Now Rust as a target for compiling proofs into a programming language is pretty nice. Safe code can have no aliasing due to borrow checker (which should also be formally verified). Threading issues are vastly simplified, though fairness still has to be verified, as well as a few other properties.

Could this be used on the LLVM intermediate code?

http://www.cis.upenn.edu/~stevez/vellvm/

Good find. Likely yes.

look at this : https://math.mit.edu/research/highschool/primes/materials/20...

Reply on news.ycombinator.com