4 ms·

What's interesting is that (as described in the present top comment on this article, about "CALL BRIAN"), if the abstraction of "type safety" is leaky (as it is

by gue5t 11y ago

What's interesting is that (as described in the present top comment on this article, about "CALL BRIAN"), if the abstraction of "type safety" is leaky (as it is, e.g. in the presence of memory or hardware errors), this kind of paranoia can actually have real-world benefits even though you can prove the impossibility of the code running using static analysis. Sometimes the important artifact is the executable in the larger context of the deployed system, rather than the code you generate it from.

nightski 11y ago
There is nothing preventing modeling the contextual environment within static analysis. Static analysis/type systems help the programmer draw the line between the known and the unknown. Some conditions are just not practical or efficient to check for. However for the context you use it within you can make certain guarantees about the code. This is still incredibly useful even though it doesn't guarantee an error can never take place. You say it "is" leaky in the presence of memory corruption. However that is not necessarily true. One could model software memory verification within a type system. Meaning, you could guarantee at compile time that each time a variable is read it is verified via checksum against its last written value. This would not be particularly efficient, but the point stands that type systems can be used (and should be used) to model hardware failures. This is no different than network link failures, etc...
- TillE 11y ago
  And how do you verify that your checksum-verifying code hasn't been corrupted with cosmic rays? The real world is messy. We can mitigate that, but we can never have mathematical purity.
  - nightski 11y ago
    That is exactly the point, to mitigate it. Just because you can't mitigate everything doesn't mean it is less valuable. It is still extremely valuable to mitigate the things you do (or choose to) have control over.

by gue5t 11y ago

nightski 11y ago

There is nothing preventing modeling the contextual environment within static analysis. Static analysis/type systems help the programmer draw the line between the known and the unknown. Some conditions are just not practical or efficient to check for. However for the context you use it within you can make certain guarantees about the code. This is still incredibly useful even though it doesn't guarantee an error can never take place. You say it "is" leaky in the presence of memory corruption. However that is not necessarily true. One could model software memory verification within a type system. Meaning, you could guarantee at compile time that each time a variable is read it is verified via checksum against its last written value. This would not be particularly efficient, but the point stands that type systems can be used (and should be used) to model hardware failures. This is no different than network link failures, etc...

TillE 11y ago
And how do you verify that your checksum-verifying code hasn't been corrupted with cosmic rays? The real world is messy. We can mitigate that, but we can never have mathematical purity.
- nightski 11y ago
  That is exactly the point, to mitigate it. Just because you can't mitigate everything doesn't mean it is less valuable. It is still extremely valuable to mitigate the things you do (or choose to) have control over.