On 12/9/2012 1:57 PM, Obrst, Leo J. wrote:
> My point, John, is that most of these approaches require
> translation to a functional or declarative language, i.e.,
> your "depends on a special language for writing the procedures". (01)
Actually, I don't consider that a limitation at all. (02)
I agree with Alan Perlis that the task of program verification, as
it is typically defined, is worthless for most practical purposes: (03)
1. Question: What would it mean to prove that a program P
written in a language L1 is correct? (04)
2. Answer: Prove that for every input that satisfies the
preconditions stated in some logical language L2, the
result of executing P will satisfy the postconditions
stated in L2. (05)
3. For any practical program, the task of proving point #2 is
likely to be difficult or impossible -- i.e. undecidable. (06)
4. Furthermore, the task of stating all the preconditions and
postconditions in L2 is likely to be as difficult as writing
the program P. (07)
5. With a good compiler, it would be far easier to *compile*
the preconditions and postconditions in L2 to executable
code in L1 or other reasonable programming language. (08)
6. Compilation can normally be be done in polynomial time,
the result of the compilation is guaranteed to be correct,
and no verification is necessary. (09)
This doesn't mean that the research on program verification was
wasted -- because much of that research can be adapted to the task
of designing compilers from logical specifications. (010)
As examples, I would cite Mathematica as a system that mathematicians,
physicists, and engineers routinely use to develop logical (i.e.,
mathematical) specifications and translate them to executable code
-- usually in FORTRAN or C. (011)
Financial people (i.e., the "quants" who play games with the stock
market in order to rip off ordinary investors) are also very heavy
users of Mathematica. (012)
By the way, I came across the following list of other semantics. (013)
John
______________________________________________________________________ (014)
anecdotal semantics:
once I wrote this program, and it just fried the printer.. (015)
barometric semantics:
I think it is getting clearer.. (016)
conventional semantics:
usually, this means.. (017)
detonational semantics:
what does this button do? (018)
existential semantics:
I'm sure it means something. (019)
forensic semantics:
I think this was meant to prevent.. (020)
game semantics:
let the dice decide (021)
historical semantics:
I'm sure this used to work (022)
idealistic semantics:
this can only mean.. (023)
jovial semantics:
oh, sure, it can mean that. (024)
knotty semantics:
hm, this part over here probably means.. (025)
looking glass semantics:
when I use a program, it means just what I choose it to mean,
neither more nor less (026)
musical semantics:
it don't mean a thing if it ain't got that swing. (027)
nihilistic semantics:
this means nothing. (028)
optimistic semantics:
this could mean.. (029)
probabilistic semantics:
often, this means that.. (030)
quantum semantics:
you can't ask what it means. (031)
reactionary semantics:
this means something else. (032)
sherlockian semantics:
since it cannot possibly mean anything else, .. (033)
transitional semantics:
for the moment, this means that.. (034)
utilitarian semantics:
this means we can use it to.. (035)
venerable semantics:
this has always meant.. (036)
weary semantics:
<sigh> I guess that means.. (037)
xenophobic semantics:
for us here, this means.. (038)
yogic semantics:
we shall meditate on the meaning of this. (039)
zen semantics:
ah! (040)
Source: (041)
http://www.haskell.org/pipermail/haskell-cafe/2011-January/088315.html (042)
_________________________________________________________________
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 (043)
|