Need for Formalism

[Sid Askary <saskary@nuperus.com>]

I would like to pose the need for a ”formalism” to the group.  I think we 
need it.  Here are some of my thoughts.  Let me know what you think.

When developing a programming language (be it declarative, as in the case 
of BPEL), there is generally a computation model (reasoned mathematically – 
as is the case with process calculi) followed by syntax and semantics.

The syntax will usually be accompanied by one or more of the three commonly 
known complementary formal approaches:

1)  Denotational semantics: -  Used mainly for requirements, specification 
correctness, etc.
-  Concerned with effects - observable behavior (and property) after 
execution.

2)  Algebriac Semantics:
-  Used mainly to reason about the language specification.
-  Concerned with partial correctness – formulas for pre and post condition 
states.

3)  Operational Semantics:
-  Used mainly for guidelines on implementation.
-  Concerned with how to execute a program using atomic steps and 
transition rules.

The above methods are neither always present in a language presentation, 
nor are they complete.  For instance, “Total correctness” proofs such as 
deadlocks, abnormal termination, etc. are often ignored.  Nevertheless, 
they help to reinforce the soundness of the proofs (or claims) by multiple 
means.

The issue of formalism becomes even more critical when a language is being 
debated in the context of a standard organization.  And in the case of BPEL 
specification, although there is a notion of “operational semantics” 
(albeit not formalized), there are also “distributed”, “concurrent” and 
“asynchronous” properties that are not formalized – (“intent” and “goals” 
notwithstanding, as I look forward to reading that upcoming document from 
the original authors).  Since the BPEL specification is a combination of 
XLANG and WSPL, what is the combined computational model?

To relegate this question to practical domain is not sufficient.  It is 
often the case that in practice, such problems are tackled empirically in 
execution environment where common programming languages (and/or platforms) 
can simultaneously mask some deficiencies AND highlight others in the 
specification.  Furthermore, while they may focus on common to perform 
process/workflow patterns, the implementations do not reflect the causal 
relationship for stratification of specification as it pertains to certain 
aspects (i.e. reliance on certain protocols, security, choice of 
methodology for extraction of expressions, etc.).

Therefore, two additional semantics plus a computational model is needed in 
order to fully reason about the specification and discuss provability, 
completeness, liveliness and other relevant properties.  I imagine that the 
original authors have some or all of these constructs and I only ask that 
they be shared with the group.

Regards,
Sid Askary