Soundationalists

Soundness is a much-maligned metatheoretical property.

To the theoretician, soundness is an obvious given: if your theory is not formally sound, it is useless. To remind the reader, a logical theory is sound if and only if its inference rules prove only formulas that are valid with respect to its semantics. In most cases, this means that its rules have to preserve some notion of "truth," so that in each step of a proof, validity is preserved. Even wikipedia says, "Soundness is the most fundamental property in mathematical logic."

To the practitioner though, soundness is a desirable, but not necessarily mandatory, property enjoyed by few tools. Most tools that are "sound" end up being too difficult to use, as they have too many seemingly arbitrary restrictions due to assumptions made in defining the underlying theory (e.g., Spec#), or they require interactive use by experts (e.g., the LOOP tool).

In counterpoint to these "sound" tools (more on the use of those double quotes later), automated tools that require little intellectual or fiscal investment are the only tools that are broadly adopted and make an impact in recent years. But automation comes at a price, and for complex systems analysis, that price is usually soundness.

Unfortunately, this second perspective is lost on many theoreticians. They not only insist that soundness is a mandatory property for a logical theory—the quality research of mathematicians who develop deviant (non-classical) logics and paraconsistent logic systems notwithstanding— they also demand that all tools be sound and that any tool that is not sound is worthless. I call these kinds of researchers "soundationalists".

I have several problems with the soundationalist point of view.

Firstly, the soundationalist is forcing a value judgement on others. Inconsistent systems are all around us, and yet we, as humans, work with and within them everyday, with aplomb. Formal mathematical systems, whether they are logics or tools build upon logical foundations, are no different. The humans that work with such systems will adapt to their particular quirks, whether the quirks are harmless idiosyncrasies of operator precedence or more serious challenges, like the fact that a particular theory has dangerous corners that are not know to be sound. Remind the soundationalist of the consistency issue with set theory that they will quickly change the subject.

Secondly, I find that very few soundationalists have practical experience in building or using tools grounded in formal theoretical foundations. They are often the researchers who claim that translating a theory into practice is "just a matter of engineering." Thus, my problem is that the soundationalist has lost their connection with the "reality" of our discipline.

Alternatively, they are the ones that delegate the dirty job of realization (i.e., implementation) to their graduate students, never involving themselves in issues of architecture or programming, and then proclaim that their software is sound because their theory is sound.

Whenever I heard this claim I immediately presume the speaker does not know what they are talking about or they are trying to mislead me. The myriad of design and implementation choices, trade-offs, and challenges that accompany implementing any formally grounded software system leave dozens, if not hundreds, of soundness compromises to creep in. In my entire career I have yet to see the implementation of a sound formal system result in a sound formal tool with an accompanying mechanical proof of soundness of both claims.

Lastly, the soundationalist is ignoring reality. Non-trivial tools grounded in formal systems must make compromises if they are to be automated, since very few interesting and useful problems are decidable in the first place. A verification system that attempts to handle simple arithmetic is already over the precipice; one that claims to reason soundly about procedural or object-oriented programs—programs that are the concrete realizations of some of the most complex mathematics ever invented by man—is simply being specious.

I propose an alternative strategy to dealing with soundness.

First, by all means attempt to develop sound logical theories, but do not shirk your responsibility in proving your theory sound. A hand-waving proof in a short paper is persuading only to the persuaded. Mechanically formalize your theory in an appropriate logical framework and show how smart you are by closing the book on soundness by developing a watertight soundness proof in all its gory and glorious detail.

Secondly, learn a little bit about alternative, possibly unsound, strategies in developing and using non-traditional logics and logical frameworks. There are so many interesting pieces of work out there with broad application, ranging from Haack's survey of deviant logics [1] to paraconsistent logics' use in knowledge representation, abductive reasoning, and belief logics [2-6].

We need to see more mechanized work in these logic. I would love to use or develop a non-classical model checker. The application of paraconsistent reasoning to the hard problems plaguing (or, more commonly, ignored by) those working in the "semantic web" and "agents" research areas represents some interesting, novel, and non-trivial low-hanging fruit for the right research team.

Lastly, if you build a tool based upon a sound theory, (a) document every design and development decision you make that possibly compromises soundness and (b) make it a mandatory feature that your tool has a metatheoretical warning system, much like ESC/Java2 does [7]. Your users will be better informed about the reasoning that they are actually performing and they will better understand the concessions that they must make to use your tool for its intended purpose.

Also, of course, you will be more honest about your scientific product, and everyone likes a self-deprecating scientist that spends serious intellectual effort pointing out their own flaws and their competitors successes.

[1] Susan Haack, Deviant Logic. Cambridge University Press, 1974.

[2] G. Priest and R. Routley and J. Norman, Paraconsistent Logic: Essays on Inconsistent. Philosophia, 1989.

[3] Max Urchs, Essays on Non-Classical Logic, chapter "Recent Trends in Paraconsistent Logic." World Science Publishing, 1999.

[4] Diderik Batens, Frontiers of Paraconsistent Logic. Taylor and Francis, Inc., 2000.

[5] Diderik Batens, Paraconsistent Logic: Essays on the Inconsistent, chapter "Dynamic Dialectical Logics." Philosophia, 1989.

[6] C. Damasio and L. Pereira, Handbook of Defeasible Reasoning and Uncertainty Management Systems, chapter "A Survey of Paraconsistent Semantics for Logic Programs." Kluwer, 1998.

[7] Joseph Kiniry, Alan Morkan, and Barry Denby. "Soundness and Completeness Warnings in ESC/Java2". The 5th International Workshop on the Specification and Verification of Component-based Software (SAVCBS 2006). Portland, Oregon. November, 2006.