Re: Alloy paper



Date view Thread view Subject view Author view

William Frank (wff@fsarch.com)
Sat, 29 Jul 2000 11:39:41 -0400



At 09:07 PM 7/28/00 -0700, Joaquin Miller wrote:

The biggest practical problem with informal systems is that they allow us to argue endlessly.

The one practical problem with formal systems is, of course, that they have no meaning at all.  But the terms of a modeling language in use do have meaning.  It is easy for a human observer to learn the meanings by watching.

And by informal but precise explanation of the meaning.  

I feel the two camps Robert describes are both off target. 

I agree with this, in that there is a difference, which Joaquin has pointed out, between precise and formal. Also, what is needed not so much as a formal system is what formalists know about, namely the methodology of mathematics, science, and engineering, so that we can apply well established principles for explaining the meaning of fundamental terms, constructing defined terms, distinquishing clearly between definitions and things which follow from the definitions, etc.  

What is needed is work along the lines of what was done with RM-ODP.  The UML needs a clear and clean specification in ordinary, informal language, which specification is solidly based on a formal foundation.

I agree almost all of this: the second sentence complete. The first one if read carefully.  But it is dangerous to hold ODP up, in my mind, as the example, because despite the fact that it has the properties described in Joaquin's second sentence, it is remarkably unapproachable, partly because it hides its foundations.  It does not explain its own methodological scheme, and it has taken me a half a year to figure out just how sound and standard, from a methodology of science point of view, that scheme is.   I have found that many computer scientists, in a desire to, in my opinion, to seem macho and ape their mathematical brethren, have a particular bent for obscuring their intuitions in a blaze of formalism, so that you have to dig through all the formalism to figure out the value of what they are saying.   The best mathematicians are not that way.  And I think that ODP suffers from a bit of this.

[Joauqin] The thing to do is to develop a formal system, beat it into shape, then translate it into a set of natural language concept "definitions."  These so-called definitions will be like those in a dictionary.  Either there will be circularities or the definitions will use undefined terms, or both.


[That's as it should be.  Remember, as Bunge said, if there is one thing that twentieth century philosophy has taught us, it is that we can not define everything while avoiding circularity.]

Some of the UML 2 workers will welcome help from formalists.

Again, agree completely but I am afraid of the fact that in computer science, many "formalists" are only that.   I think that we need help from logicians and scientific methodologists, or people well-schooled in these subjects, but ones interested in the applications of these topics, and less interested in developing formal theories than in applying what the world knows about how theories should be developed, to make them consistent, not circular, useful, and complete as possible.  The problem with this, in terms of getting help where you might expect it, is that it is not "original" research. 

For example, the issue of discussion of the last week, concerning the relationship between associations and references, could be much clarified by a consideration of model theory and set theory, but needs some mathematical observations, not someone spinning a big formal system based on a particular view. 

For another example, the work on provably correct programs has had, in my opinion, its most significant impact not on those very few programs that have ever been proved to be correct, but on the *style* of programming.  If programs are written in a manner in which it is *possible* to prove them correct, even if the proof is not attempted, it is more likely that they *will* be correct, as thier meaning and implications are more transparent to the human mind.  Thus,the immense value of this work for the engineering community has been somewhat indirect. 



[We also need to provide as much compatibility with UML 1.4 as reasonably can be provided.  It's not nice to abandon your installed base.  This can be done, but not if it is not attempted.]

Aha.  I can see that this would be very important, and a very good argument for constructing a formal theory, to understand the problems of maintaining "compatibility", and defining exactly what we need there.


Cordially,

Joaquin Miller
Chief Architect
Financial Systems Architects

mailto:joaquin@acm.org

San Francisco
phone: +1 (510) 336-2545
fax:   +1 (510) 336-2546
PGP Fingerprint:
CA23 6BCA ACAB 6006 E3C3 0E79 2122 94B4 E5FD 42C3


Date view Thread view Subject view Author view