> A procedure is fundamentally different from a function from a reasoning-about-the-code perspective.
They really are not unless the langage puts specific limitations or features on one or the other.
And odds are the average “procedure” should not be one, because it only exists for its side effect but then provides no feedback about these side effects.
1. In the older versions of Ada standard, functions can't have side effects, in a sense that they are not allowed to return more than one value (by setting the function's parameter's mode to out). Procedures always allowed to have side effects.
2. Functions can be expression functions which can be set in the code specification or used in expressions. Procedures can be written only in packages' bodies.
3. Procedures can be set to no-return state: that kind of procedure doesn't end in the normal way, but, for example, only by raising an exception.
4. Procedures can be null procedures, empty. That not the same as abstract subprograms from other programming languages.
Also, the difference is, in my opinion, more visible in the safe subset of Ada, SPARK, where still exists the rule which forbids side effects on functions.
GP 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
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.
As a pedant myself, i find this rather pedantic. Language use evolves and insisting it is only correct when words are used with their original meaning won't win you much. If you distinguish between produres and functions or functions and effects, many will get what you mean and it is more elegant IMSubjectiveO.
Same goes for im/mutability, i think val/var is more elegant than let/let mut but that is only my opinion on aesthetics. I like good design but still think function is more important than form.
The "pure" functions have different properties with respect to program optimization and program verification, in comparison with the functions or procedures with side effects.
That is the reason why this distinction matters. The distinction between mutable and immutable variables matters for the same reason.
Otherwise, the difference between a "procedure" and a "function" with side effects where you ignore the return value has no practical consequences.
There are contexts where you do not care about the optimizations that can be done by the compiler or about program verification, but there are also contexts where you care.
> Why would we? And how should they be different, and what useful properties would that provide?
Functions should be similar to mathematical functions and come with guarantees like purity, referential transparency, and totality.
Another reason they should be different is they've got different names! Might seem trite to say that, but what's the point in having the same concept with different titles?
Pure functions are very powerful concepts, especially when it comes to composition, if the consumer of a function can't rely on that, then the consumer must investigate the internals to know what it does. Once you're several layers deep into your composition that becomes exponentially harder to do.
So, there is value to having a concept (with a suitable name, like 'function') that indicates to the consumer what it is they're dealing with. Some languages, like Haskell, bake this in; others like JS really don't - making the whole process of dealing with 'functions' (really procedures) much harder once an application is more than a toy project.
> Functions should be similar to mathematical functions and come with guarantees like purity, referential transparency, and totality.
Essentially none of that is embodied in Ada's distinction between functions and procedures though, despite that being "fundamentally different […] from a reasoning-about-the-code perspective" according to the comment I replied to.
The only thing Ada tells you is "this definitely has side-effects" because there's no other reason to have a function without a return value, but that's the least useful thing you can be made aware of.
> Another reason they should be different is they've got different names! Might seem trite to say that, but what's the point in having the same concept with different titles?
Because you're very confused and making a distinction between things which are not different?
> Pure functions are very powerful concepts
That's debatable, but even then it's not what function means in Ada.
> especially when it comes to composition, if the consumer of a function can't rely on that, then the consumer must investigate the internals to know what it does.
Knowing what a function does is probably a good idea either way. You can call `map` with the same parameters as `filter` but the result will be rather different.
Initially, Ada had the restriction that the functions must be pure.
The restriction has been lifted only much later, so what you say is correct for modern Ada, not for the original Ada.
While gcc and other C and C++ compilers have non-standard extensions to specify whether a function is pure or not, I assume that an Ada compiler can recognize a pure function just by the fact that all its parameters are "in", so no extra keyword is needed.
What is needed is that the pure functions must be easily recognized by compilers and other tools and also by programmers. Not only there is no need that the functions be restricted to pure functions, that is actually undesirable.
AFAIK, unlike in C/C++, where pointers can make this task quite complex, in modern Ada it is still easy to recognize the pure functions.
They really are not unless the langage puts specific limitations or features on one or the other.
And odds are the average “procedure” should not be one, because it only exists for its side effect but then provides no feedback about these side effects.