3 ms·
I didn't say anything about types. :) I said functionally equivalent. What it means depends on the definition of "functionally equivalent" of course. The fir
by Drup 9y ago
I didn't say anything about types. :)
I said functionally equivalent.
What it means depends on the definition of "functionally equivalent" of course.
The first version, which is types, is the most immediate and obvious, but as you pointed out, not that useful.
Abstractions, however also works at the semantics level: if A behaves like B trough the interface S, then you can confidently say that for any F (of type S -> S'), F(A) behaves like F(B). So you can just test that A and B are not distinguishable (property testing is very good at this) and feel confident about your refactoring!
The definition of behaves like depends on your language. Usually, this doesn't account for performances, as you point out, but only for the observable semantics. This is known as parametricity[1]. If you really want to get into the deep end, [2] demonstrates all that for a (very rich) ML module system.
[1]: https://en.wikipedia.org/wiki/Parametricity https://en.wikipedia.org/wiki/Parametricity
[2]: http://www.cs.cmu.edu/~crary/papers/2017/mapp.pdf http://www.cs.cmu.edu/~crary/papers/2017/mapp.pdf
- skybrian 9y agoGood point! But leaving types aside, the same argument applies. "Observable semantics" seems to mean "observable according to our semantic model" which is an agreement to pretend that machine behavior outside the model isn't observable and avoid relying on it. This agreement is normally a good thing since it's what allows for the same program to run on different machines, or to compile the same program with different optimizations, or swap in a newer version of a library with a better hash function and claim it doesn't break backward compatibility. Nevertheless, it can be a blind spot as we saw with Meltdown and Spectre, so I wanted to emphasize that this is a useful myth but the world isn't obliged to go along with it. It's often important to observe program behavior that isn't specified by the language.
- Drup 9y agoAh, yes, This is where safety and security differs! Abstraction is about safety: preventing errors and giving additional guarantees, not preventing attacks. :) Nothing I said hold when people are being malicious: Even in OCaml, you have escape hooks that allows you to break past abstraction boundaries and do whatever you want.
- skybrian 9y agoAgreed, but this is where our own jargon betrays us: in ordinary usage by non-programmers, "safety" includes safety from attacks. Perhaps especially from attacks?
- Tomte 9y agoOrdinary usage is often murky, but the usual distinction between security and safety is not whether it is about an attack, but about the direction of the threat. Safety means the environment is not harmed by the system. Security means the system is not harmed by the environment.
- nickpsecurity 9y agoThat's an interesting definition. Traditionally, we had several ways of looking at it: 1. Safety contends with accidents like components breaking. Security contends with malice where input is crafted and failures are set up intelligently to do damage unlikely to happen on accident. There's quite a bit of overlap, though. 2. If talking leaks, safety rarely requires confidentiality of data. It's usually integrity or availability that it shares with security. So, a security violation with covert/side channels might not be a safety violation. Just two off top of my head to illustrate the difference.
- lmm 9y agoI think of it the same way you'd think of it in a workshop: a "safe" drill or saw is one that can be used in a safe way, not one that's safe from deliberate attacks.
- nickpsecurity 9y agoThere's work to address that. Look into proof-carrying code and "fully-abstract compilation." There's also been proofs done for hardware and assembly against specs in ACL2 and Abstract, State Machines.