Paul & All:

Given the recent release of OSD’s Digital Engineering Strategy [1] I thought this a good time to start a discussion on models and formalization.

Some may be surprised to learn that among insiders in government architecture the juxtaposition of the terms “model” and “formal” are considered an oxymoron. Mainstream efforts by well-known consortia lack formality. Even DARPA programs such as META from which Cyber Physical Systems reveal lack of formality.

“Parametric and Logical Types for Model Driven Engineering” [2] in which section V. Proof Calculus for Logical Types provides a formalization of parametric conjunctive and disjunctive types in a constructive logic.

I look forward to a lively discussion.

1. https://www.acq.osd.mil/se/docs/2018-DES.pdf
2. http://rickmurphy.org/params.pdf

Topic

[capatchModerator]

Hi, Rick!

Thanks for starting the conversation and offering the latest guidance and your work to review/discuss. We’re mostly on the road right now, but wanted to let you know that we’re taking a look at the docs before diving in. I hope other members of the community will digest and jump in a well.

Sincerely,

Cully

CSIAC (DoD Contractor)

• This reply was modified 10 months, 2 weeks ago by  capatch.

[rickmurphyParticipant]

I suspect some or possible most folks are scratching their heads on the paper.

I am happy to answer questions.

Let me share a story on “model formalization.” A well-known standards development organization recently formulated a new standard with a mandatory requirements that proposals must be “grounded in a formal logic.” The purported “formal logic” was itself a standard approved by ISO. It contained the following statement :

“The following are outside the scope of this International Standard:
• the specification of proof theory or inference rules;
• specification of translators between the notations of heterogeneous computer systems;”

The problems were obvious to me and may be obvious to some of you. Here they are:

1. The purported “formal logic” is neither formal, nor is it a logic. See Section V in the paper for what a formal logic looks like.

2. The dependent standards development organization proposed a mandatory requirement that could never be satisfied. Therefore any customer, let’s say like DoD, who depends on the expertise used in the development of standards, is subject to “caveat emptor.”

I look forward to further discussion of “model formalization.”

[Author]

Replies