> 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.