5 ms·

How do you address the inherent unsafeness of hardware? Even "pure" functional languages are hacking around this...

• pjc50 11y ago
  Elaborate on what you mean please?
• johnbender 11y ago
  Assuming you mean the weak memory models, the compiler normally enforces the guarantees made by the semantics of the programming language ... assuming you have a semantics. That's where this project comes in and that is why the C++ memory model definition/formalization was so important. Programmers need to know what guarantees the compiler gives about the behavior of the code after compilation and the semantics is the final word.
• GolDDranks 11y ago
  What do you mean? Do you mean that hardware is unreliable or might break and thus even a sound program, or a program that doesn't do anything that counts as unspecified behaviour, is not 100% safe? Or that with "unsafe" escape hatches often needed to directly interop with hardware are a problem?
  • GolDDranks 11y ago
    If it's the former, I agree. If it's the latter, well, in Rust, the norm is to design safe abstractions around unsafe code. For example the vector class of the Rust standard library contains some unsafe code, but with the all parts that are unsafe being private, the public API exposed is essentially safe. If this project comes up with reasonable semantics what can be considered to be "safe" with unsafe code, we can verify, that the unsafe bits of the standard library (and other libraries) are being used in a safe manner.
• bassislife 11y ago
  I think the assumption is that the hardware spec is correctly implemented and that it runs ideally well. Otherwise that would require some kind of probabilistic model I guess. But you're right, "purity" is a simplification. Computations are inherently effectful(and even side-effectful depending on the reference frame) in practice. Also, I seem to understand that the research is merely done in the context of the Rust language. The title is maybe a bit too much :)
• pcwalton 11y ago
  > How do you address the inherent unsafeness of hardware? Even "pure" functional languages are hacking around this... By proving the hardware correct. Then if you're running proven memory safe Rust on formally verified hardware, you're guaranteed by construction that the Rust you're writing is memory safe (for the formally-specified notion of "correct" and "memory-safe" in use, which will probably issues like manufacturing problems and compiler bugs). A Google search for [hardware formal verification] can get you started, if you're interested. There's been a good deal of work in this area.