|From:||Steven Ericsson-Zenith <steven@xxxxxxx>|
|Date:||Fri, 13 Feb 2015 17:54:52 -0800|
For me, at least, a proof is only useful in order to guarantee behavior. If the ground upon which a proof is executed is itself unable to provide or maintain such guarantees then the proof is, quiet literally, useless.
I understand where you are coming from in terms of software development. But in this case what, exactly, does such a proof tell you? Typically it is something like "The program [written in a formal language with a mathematical basis, of which there are few, but lets say it has a CSP basis] is proven to meet its specification [that is also specified in a mathematically based language (say CSP)]."
You can't do this with UML and C++, for example. Similarly, you can't do this with schema-aware XSLT or XQuery. What would it mean if you did?
The answer is that it wouldn't mean much at all. For one thing you at least need a formal specification of the target machine architecture even if you do not have a specification of the hardware. If you specify an algorithm against what do you test it?
There are, of course, desirable properties - consistency, correct syntax, valid semantic transformation, schema adherence etc... So this is not to say that automated checkers that translate between higher and lower level languages do not have merit but do not mislead yourself into believing that such checks say anything other than there is a vague (a "maybe") equivalence between the eventual behavior of the two.
The bottomline is that there are uses for checkers but these can never provide "proof" that is only ever about the behavior of a program and this behavioral integrity must go to the wire or else it is not a proof. And, of course, a proof can tell you nothing at all about the merit or otherwise of the human specification or design.
And this is where you are confused about pure mathematics. Pure mathematics may be widely applied but it does not draw in the discipline that is using it (hence "Pure"), but rather the discipline that uses pure mathematics is, in fact, applied. So thoughts of data structure and program decomposition, logical structure, distribution of types and classes, variables and conditionals, schemas are computer engineering.questions using applied mathematics.
Indeed, despite protestations to the contrary (think Chaitin, Wolfram and company), computation is itself an applied discipline that is well short of pure mathematics. Alan Turing was a master engineer and mathematician, and he was also a scientist in his exploration of morphogenesis, where he used differential equations and not computation. But let's not confuse the disciplines as a result.
There is no part of computer engineering that is purely mathematical, there is plenty of applied mathematics in computer engineering. When I say, contrary to John, that it is conceivable that computer engineering can become science I am thinking of a time when our study and understanding of cause and effect is complete, that is, when programming a construction of our making is, in fact, the manipulation of creation. At this point, we are effectively Gods. And as I said, I do see that potential in bioengineering but it seems a long way off and we need to extend our useful lifespans first.
Let me acknowledge that computing machinery is vastly more capable at certain tasks. Many of these tasks affect human behavior but aside from this what do they do? What difference do they make in the world? Well, they have enabled us to send craft into the local planetary system and out into intersystem "space", a small beginning. But what is the role of intelligence in the universe as a whole? At this point, it seems there is none.
Except biophysics offers the potential that the role of intelligence is to place life where it would not otherwise appear. This is the best I can come up with right now. Although the ethical issues and social motivations of this pursuit seem insurmountable.
One of the profound limits of current computational models is in its discrete nature. Its inability, for example, to embody anything of relevance to the human mind. We are dealing with a machine, it consists of collections of simple mechanisms, and lots of them, all of which are related by a fragile artificial composition of our design constrained by polynomial time.
These collections are unsuited for independent survival in their environment. And as pretty and as powerful as they seem, they are short lived, unproductive, tomorrows junk. None have the resilience and longevity of the bio world, they do not reproduce themselves, they do not repair themselves, without us they are nothing at all.
Yet they have the richest of us wasting our time and resources in fear of the bogey man (Musk , Gates, etal.). I have friends that have spend decades of their careers building software for systems that they claim may become "self-aware," and I keep telling them that their efforts are futile in the face of these considerations.
There is no across structure decision making, there is no holistic recognition, there is no responsive motion in the vast majority of computing systems, there are only bits - and this is simply the wrong paradigm.
That said, it is clearly surprising that we can create and imbue such machines with aspects of our intelligence, but this is a reflection of our own ingenuity and Wigner's observation concerning the unreasonable effectiveness of mathematics, but this surprise must not lead us astray.
On Fri, Feb 13, 2015 at 9:49 AM, William Frank <williamf.frank@xxxxxxxxx> wrote:
_________________________________________________________________ Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/ Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/ Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx Shared Files: http://ontolog.cim3.net/file/ Community Wiki: http://ontolog.cim3.net/wiki/ To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J (01)
|<Prev in Thread]||Current Thread||[Next in Thread>|
|Previous by Date:||Re: [ontolog-forum] master data vs. ontologies, Ravi Sharma|
|Next by Date:||Re: [ontolog-forum] master data vs. ontologies, Steven Ericsson-Zenith|
|Previous by Thread:||Re: [ontolog-forum] master data vs. ontologies, William Frank|
|Next by Thread:||Re: [ontolog-forum] master data vs. ontologies, Steven Ericsson-Zenith|
|Indexes:||[Date] [Thread] [Top] [All Lists]|