Lambda the Ultimate

foo

Ask a real question.

He asked a "real" question, even if one thinks that it's obvious or irrelevant, so please refrain from using such harsh tones, it's against our policies here.

Didn't sound harsh to me when I wrote it but I take your point.

Being "sure" about something isn't good enough. Of course one would like to assume that function composition preserves semantics. But how do we know for sure? This is a property that might or might not hold for a particular language and implementation. What would it take to be really sure? Should we really just take it as an axiom? Many equally obvious transformations hide serious problems.

I am certain that the original question was formed sufficiently ambiguous that it amounts to a rorschache test (i.e., an accidental or otherwise "troll"). I tried to point that out with "flourish" but instead came off as obnoxious. My bad.

It is a confusing question. I was also aware of that. But why is it confusing? That is interesting also. Perhaps in software we need to think about semantics more than we are accustomed to in other areas.

It's confusing because you don't specify what you mean by "correctness" of the components nor what it "correctness" of the composition means. Your question is dramatically underspecified. It's well understood in software engineering that you can only speak of correctness with respect to some specification. Something isn't correct or incorrect on it's own. A correct implementation of a sorting algorithm is an incorrect implementation of string concatenation. Their composite is only correct if it produces the desired behaviour. Even if the components fail to meet their specifications (are "incorrect") their composite may still meet it's specification. Thus, the correctness of a composite (in this sense) neither is determined by nor determines the correctness of the components.

Using more general (partial) specifications such as memory safety or type safety, these questions can't be answered without a semantics, but usually are answered (when they are considered at all) given a semantics.

Certainly specification is very important but I would add that specification and semantics can be closely related. In the ASM method we can specify a sorting algorithm but the result is actually a semantics. This is because the ASM codes, which are not necessarily executable, are in terms of a "ground model" which is a "first order algebraic structure". We could get to an executable by "refining" the ground model "isomorphically". The system and it's correct use by following the axioms is guaranteed to produce a consistent semantics satisfying the original "specification".

Also specification can imply more than execution semantics, and there is an issue of how one translates specifications which could be economic or cultural into code.

Lastly, I am not recommending any of this but currently just trying to learn more.

Interesting paper. Functional systems, languages, actually do have many interesting modeling interpretations because they look a lot like final systems as in systems theory. The morphism from a system with explicit state to a functional system is final (or close at least) From a modeling point of view deconstruction is also interesting.

Typically if we can put the "things" into a consistent semantics we are on solid ground.

Right. A major point of formal semantics is to provide provable guarantees about things like compositionality.

(Although I'll note that re the original question, a semantics doesn't necessarily "prove correctness" e.g. with respect to some external specification, as others have also alluded to.)

But I wonder if this can be formalized or if it must remain an art?

Are you asking whether the process of formalizing can be formalized? The likely answer is no, or at best, only partially. There's a well-known Alan Perlis quote about this: "One can't proceed from the informal to the formal by formal means."