3 ms·
https://www.adaic.org/resources/add_content/standards/05rat/html/Rat-9-3-9.html https://www.adaic.org/resources/add_content/standards/05rat/... Interesting his
by pwr-electronics 5y ago
https://www.adaic.org/resources/add_content/standards/05rat/html/Rat-9-3-9.html https://www.adaic.org/resources/add_content/standards/05rat/...
Interesting history of how there was supposed to be a difference, but the idea was dropped and then later revived by SPARK.
- masklinn 5y agoGP is not talking solely about ADA though, they are asserting that there is a fundamental difference which is embodied solely in the presence or absence of a return value which is missing from e.g. "everything is a method" Differentiating between pure and impure functions might be useful[0], but while not strictly orthogonal the presence of a return value doesn't tell you anything about that. Even ignoring the error signalling, read(2) has a return value (the data being read) and also has side-effects. [0] though it's debatable that this distinction is really useful in and of itself
- pwr-electronics 5y agoThe general discussion is about Ada ... GP said it depends on what the language does with that concept, and then I linked some extra info about what Ada and SPARK do with the concept. As for whether it's useful ... it's absolutely useful. Side effects break basic blocks. The smaller the basic blocks, the less optimization can be done. Side effects also require special handling when using theorem provers. If you can specify that something should be free of side-effects, it's less work to requalify the system after making changes. The purpose of SPARK is to be formally proven, which is why it implements the feature.