5 ms·

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

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

pjmlp 10y ago
This tradeoff wasn't already an issue with languages like Modula and Ada.
- bluejekyll 10y ago
  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.
- staticassertion 10y ago
  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.
  - pjmlp 10y ago
    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.
    - staticassertion 10y ago
      OK, I should have said garbage collector, not runtime.
- bquinlan 10y ago
  Are you claiming that Module-2 is memory safe? What about: MODULE Boom VAR Foo : POINTER TO INTEGER; BEGIN Foo^ = 123; END Boom.
  - pjmlp 10y ago
    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).
AstralStorm 10y ago
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.
- bluejekyll 10y ago
  Could this be used on the LLVM intermediate code? http://www.cis.upenn.edu/~stevez/vellvm/ http://www.cis.upenn.edu/~stevez/vellvm/
  - AstralStorm 10y ago
    Good find. Likely yes.

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

pjmlp 10y ago

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

bluejekyll 10y ago
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.
staticassertion 10y ago
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.
- pjmlp 10y ago
  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.
  - staticassertion 10y ago
    OK, I should have said garbage collector, not runtime.
bquinlan 10y ago
Are you claiming that Module-2 is memory safe? What about: MODULE Boom VAR Foo : POINTER TO INTEGER; BEGIN Foo^ = 123; END Boom.
- pjmlp 10y ago
  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).

AstralStorm 10y ago

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.

bluejekyll 10y ago
Could this be used on the LLVM intermediate code? http://www.cis.upenn.edu/~stevez/vellvm/ http://www.cis.upenn.edu/~stevez/vellvm/
- AstralStorm 10y ago
  Good find. Likely yes.