Writing correct lock-free and distributed stateful systems in Rust, with TLA+

Re:Writing correct lock-free and distributed stateful system... by nonsince on Saturday May 20, 2017 @01:31AM (#14381184)

If I understand the abstract correctly, that relies on having a trusted compiler, which assumably would have to be bootstrapped ultimately from a trusted hand-written compiler in machine code. This effectively counters malicious trusting trust attacks but does not effectively counter trusting trust attacks due to error, because your entire trusted stack has to be correct.

That's not to say there's no way to close the loop here, simply that I don't know that this is it.

[ Parent | on HN ]

Re:Writing correct lock-free and distributed stateful system... by dllthomas on Saturday May 20, 2017 @12:26PM (#14383104)

You don't understand the abstract correctly. It relies on having compilers from diverse sources, unlikely to share the same malicious modification. It does not rely on any of them being trusted.

[ Parent | on HN ]