Formally truthful

Ah, what a mouthful. Meaning what?

From CACM article,
Formally Verified Mathematics

The CACM, April 2014, had an article about formal approaches to mathematical proofs. It was titled Formally Verified Mathematics and is readable on-line (image is from the article). Now, this article struck me, for several reasons, motivating this post.

The context? The proliferation of apps (see thoughts on algorithms) ought to be a concern. The auto industry seems to live more with recalls than not (many times, "computer" and "software" appear in the explanation). We just had a bad financial failing from which only the manipulators recovered (and they're at it still, yes HFTers - riggers by any other name, are riggers). The litany is depressing to behold.

Now, the authors (Jeremy Avigad and John Harrison) provide a nice overview of the issues. They actually mention the work of many (who's who) who have looked at the issues. To be brief, we have several things leading to the fact that proofs are difficult and not possible computationally without human assistance (we really need to discuss man-in-the-loop imperatives, in this case).

But, how does one get such human assistance? As, with the growing awareness of singularity (big S - actually, there are many singularities - Remarks, 05/19/2013), we get to where the computer does things that are not understandable by humans. In short, take code, do you know what it does without running it through some parse/execution device? If you do, it would have to be some trivial stuff (let me generate something very effective using rewites, etc., and then look at the code - all sorts of other methods can be proposed).

So, yes, mathematicians have interactive approaches, with supporting tools. This means that we get to a state where the computer is essential (we actually got there a long while ago - how could such an important thing devolve into a game'd affair?). In one example, they talk of a proof that was 255 pages (journal style) in the '60s for a theorem. Of course, such proving took a lot of time to state; too, it took much effort to verify.

Now, the computer can help in the verify step being faster than us in lots of way. Smarter? No way. We'll get to that (again and again). It's a "being" issue, folks.

Now, that 255 pages can be done with 150K lines of code (talking fairly terse stuff here). But, even then, a lot of stuff is not expressed but it implied with rules. Definitions, and such, would be mostly explicit.  

---

Where are we going with this? You see, mathematics does involve rigor. Formal systems are a part of mathematics, in certain senses. Computational systems are formal (yes, they are, even if it's ignored at the level of the user). Yet, we have people spawing off system willy-nilly; even the big folks do this (tsk, tsk) as the end user can be the tester.

Now, this whole thing is not to argue for being more formal and slow. Rather, we really need to get a handle on the operational aspects (beyond agility, young ones, okay?) such that we have a better handle on risks. Anyone care? Yes, those who get hurt by these types of failures. Those who are dependent upon such or who care for such.

How ought this be done? Very good question. But, my put is to propose that such techniques would very much intersect with the issues of truth engineering. So, there is one little bit about motivation for all of this stuff in this blog.

---

In that same issue of the CACM were some interesting (and related) articles. I've listed some of them by title (some may not be publicly readable on-line - requiring an account).

• Unifying Functional and Object-Oriented Programming with Scala - the surprise was use by several web vendors (those who provide something cloud-wise). For example, LinkedIn switched to the approach. 
• Security and Privacy for Augmented Reality Systems - timely, yes, and, of note, especially in regard to looking forward to issues rather than trying to cope after the fact. Perhaps, as the web user mature, and get away from the frills and titillation, we can get to more looking at more reliable types of things. 
• Re:Search - Here are two blogs by Ken MacLeod (The Early Days of a Better Nation, Ken MacLeod Writing). The former resonates, as, in another context, I'm looking at the early days of this nation (that in which I sit writing). 

Remarks:   Modified: 01/23/2015

05/30/2014 -- The May CACM (Vol. 57, No. 5) had an interesting article title "Understanding the Empirical Hardness of NP-Complete Problems" in which the authors talk about helping resolve hardness, somewhat (taming the beast), via statistical means (in terms of things, like SAT-solvers). Makes one almost thing that these issues are of no concern going forward (throw computational power at the problem). But, it cannot be as easy as that (to wit, at the end of the 18th century, the Illuminati was claiming that everything was known about physics - so everyone go home and twiddle your thumbs). As the authors say, has to do with whether you can get solutions and whether you can do so in a reasonable time. Yet, there is more (still to be characterized). If the spaces quake, solutions become more difficult. Say what? Yes, we'll be getting back to this.

01/23/2015 -- Software? Well, we are talking more than apps (latest craze). We are dealing with fundamental questions which, then, gives rise to normative issues in mathematics (and, by extension, to the computational).