3 ms·
> 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.
by 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 agoThe 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 agoRegarding 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.