5 ms·

>Using this library, you can implement bi-directional process communication with compile-time assurance that neither party will violate the communication protoc

>Using this library, you can implement bi-directional process communication with compile-time assurance that neither party will violate the communication protocol. No, you cannot. "Assurance of not violating communication protocol" and "process communication" together are an oxymoron. If you do this, you deserve all the possible failures that come along with it. Please don't write infrastructure code that depends on "assurances" instead of checking and validating communications.

theoh 8y ago
This is about validating code, not about maintaining the integrity of the system in the presence of corruption or a party that is deliberately trying to break things. It's actually helpful to be able to check that the system is sound in theory. Nobody is suggesting that you can use that as an excuse to get sloppy.
empath75 8y ago
It’s about validating that your own code matches the spec. Not validating that anybody you’re communicating with does. Though if you wrote the client and the server then you know that both do.
myWindoonn 8y ago
I wish I knew how to get this point across to people. The way I think of it is that a type-checker which validates a single program at a time isn't capable of proving certain facts which hold when access to filesystems or networks are involved.
- codebje 8y ago
  All validation is only performed up to an assumed platform. There's usually little value in worrying too much about how a real platform won't correspond precisely to that assumed platform, since the goal of validation is to remove a class of errors, not all errors.
  - rocqua 8y ago
    I think OP's point is that getting these assurances doesn't mean you can stop checking for errors that come from outside the platform.
Groxx 8y ago
Due to e.g. kernel or hardware bugs? Or something that can be ruled out in some scenarios, e.g. malicious processes?
pcwalton 8y ago
Consider that "compile-time memory safety" is still a reasonable concept, despite the fact that ptrace() means that anybody could technically read and write arbitrary bits in your process. Or that rowhammer could cause memory-safety-violating bit flips. It's the same idea here. Obviously nothing can stop, say, faulty network hardware from causing protocol violations. But that doesn't stop us from meaningfully saying that, under the correct set of assumptions, protocol violations are statically prevented at compile time.

theoh 8y ago

This is about validating code, not about maintaining the integrity of the system in the presence of corruption or a party that is deliberately trying to break things. It's actually helpful to be able to check that the system is sound in theory. Nobody is suggesting that you can use that as an excuse to get sloppy.

empath75 8y ago

It’s about validating that your own code matches the spec. Not validating that anybody you’re communicating with does. Though if you wrote the client and the server then you know that both do.

myWindoonn 8y ago

I wish I knew how to get this point across to people. The way I think of it is that a type-checker which validates a single program at a time isn't capable of proving certain facts which hold when access to filesystems or networks are involved.

codebje 8y ago
All validation is only performed up to an assumed platform. There's usually little value in worrying too much about how a real platform won't correspond precisely to that assumed platform, since the goal of validation is to remove a class of errors, not all errors.
- rocqua 8y ago
  I think OP's point is that getting these assurances doesn't mean you can stop checking for errors that come from outside the platform.

Groxx 8y ago

Due to e.g. kernel or hardware bugs? Or something that can be ruled out in some scenarios, e.g. malicious processes?

pcwalton 8y ago

Consider that "compile-time memory safety" is still a reasonable concept, despite the fact that ptrace() means that anybody could technically read and write arbitrary bits in your process. Or that rowhammer could cause memory-safety-violating bit flips. It's the same idea here. Obviously nothing can stop, say, faulty network hardware from causing protocol violations. But that doesn't stop us from meaningfully saying that, under the correct set of assumptions, protocol violations are statically prevented at compile time.