3 ms·

Having never used rust and having barely used C, here are some uninformed opinions. A memory safe language for the kernel doesn't seem possible using "traditio

Having never used rust and having barely used C, here are some uninformed opinions. A memory safe language for the kernel doesn't seem possible using "traditional" safety tools. I'd expect a "safer" language would look a lot like formal verification. If you can make a safer language that doesn't look a lot like formal verification, you can probably automate a lot of formal verification. There are still some big advantages to rust. By explicitly marking unsafe code, you've made it a lot easier to figure out what needs to be focused on. I imagine you can even formally verify just the unsafe parts of your ecosystem. Also, rusts tooling just seems more pleasant.

pjmlp 9y ago
ESPOL for Burroughs B55000 in 1961 already allowed for some kind of safety. It was a systems programming language based on Algol and already had the notion of unsafe code for low level code. Those modules had to be marked as UNSAFE and could only be executed if allowed to do so by the sysadmin. Similar exemples could be provided about PL/S, PL/8, Mesa, Modula-2, Modula-3 and many others. One big contribution that Rust brings into the table is to educate a whole generation that belives the myth that C was the very first systems programming language, that there are actually safer alternatives.
- catnaroek 9y ago
  > Those modules had to be marked as UNSAFE and could only be executed if allowed to do so by the sysadmin. Safety vs. authorization are completely orthogonal. The former is an objective property of a program, to be established or refuted with formal proof. The latter depends on the subjective whims of one specific human being, in this case, the sysadmin. And, in my experience, the typical sysadmin is not a good enough semanticist to determine whether a program is safe or not.
  - pjmlp 9y ago
    The point being that unsafe code had to be marked as such to be compilable and that tainted the binary, which was only allowed to execute after given permission. Formal proofs can also contain logic errors. Any kind of safety improvement is better than what C offers.
    - catnaroek 9y ago
      > The point being that unsafe code had to be marked as such to be compilable and that tainted the binary, which was only allowed to execute after given permission. And my point is that this is useless in the absence of someone or something capable of reliably determining whether the code is safe to run. > Formal proofs can also contain logic errors. So you have competent people write them.
      - pjmlp 9y ago
        Regarding formal proof systems, not only can they contain logic errors, they are still very far from being usable for the common programmer to do regular programming. As for competent programmer, we all know how many corporations search who they hire.

pjmlp 9y ago

ESPOL for Burroughs B55000 in 1961 already allowed for some kind of safety. It was a systems programming language based on Algol and already had the notion of unsafe code for low level code. Those modules had to be marked as UNSAFE and could only be executed if allowed to do so by the sysadmin. Similar exemples could be provided about PL/S, PL/8, Mesa, Modula-2, Modula-3 and many others. One big contribution that Rust brings into the table is to educate a whole generation that belives the myth that C was the very first systems programming language, that there are actually safer alternatives.

catnaroek 9y ago
> Those modules had to be marked as UNSAFE and could only be executed if allowed to do so by the sysadmin. Safety vs. authorization are completely orthogonal. The former is an objective property of a program, to be established or refuted with formal proof. The latter depends on the subjective whims of one specific human being, in this case, the sysadmin. And, in my experience, the typical sysadmin is not a good enough semanticist to determine whether a program is safe or not.
- pjmlp 9y ago
  The point being that unsafe code had to be marked as such to be compilable and that tainted the binary, which was only allowed to execute after given permission. Formal proofs can also contain logic errors. Any kind of safety improvement is better than what C offers.
  - catnaroek 9y ago
    > The point being that unsafe code had to be marked as such to be compilable and that tainted the binary, which was only allowed to execute after given permission. And my point is that this is useless in the absence of someone or something capable of reliably determining whether the code is safe to run. > Formal proofs can also contain logic errors. So you have competent people write them.
    - pjmlp 9y ago
      Regarding formal proof systems, not only can they contain logic errors, they are still very far from being usable for the common programmer to do regular programming. As for competent programmer, we all know how many corporations search who they hire.