Re: Cells compared to Flow-Based Programming

On Sun, 01 Jun 2008 22:31:41 -0700,
m6d01a9.3.calrobert@xxxxxxxxxxxxxxx (Robert Maas,
http://tinyurl.com/uh3t) wrote:

From: George Neuner <gneuner2/@/comcast.net>
(compared to hardware designers:)
few developers know how to formally proof software and even fewer
bother to do it except when the results will be published.

Given that it's not even possible to proof hardware, because
quantum mechanics and small impurities in materials production and
variation in physical assembly actions all make the properties of a
hardware device impossible to prove within bounds, and anything
proven from such an assumption would then be GIGO. At best
statistical estimates of success rate and MTBF (Mean Time Between
Failure) can be predicted on the basis of experience. Accordingly
complaining that software isn't formaly proofed seems an unfair
complaint in this hardware-vs-software discussion.

You clipped what I responded to which was a lament that software
couldn't be analyzed like hardware.

In any event, proofs begin with a set of postulates assumed to be
true. A software proof usually starts from the assumption that the
execution hardware will perform as spec'd.


Perhaps a more appropriate metaphor would be the legal system, of
adversarial contestants, one to show evidence for something, the
other to find flaws in the evidence leading to reasonable doubt. In
the software contest, perhaps each unit (function, method, etc.)
can be specified per initial state assumed, D/P process that
occurs, and final state claimed if the initial state was within
spec.

It's not a bad idea but


The person claiming a unit is "working" could post a demo of
the unit for testing, by both automated test rigs (some written by
an adversary) and manual/interactive attempts to make the unit
fail. If the unit has withstood a reasonable time period of such
testing, then it can be trusted. With formal specs for starting
state and final state, automated verification of matching states of
output from one unit to input of another unit, and automated
management of a whole network of such dependencies, simple
connections of the specs between units can be used to prove that
combinations would work too, without needing to test each
combination. (Maybe you're saying that the overall system for
managing such analysis of multi-unit software isn't available "off
the shelf" for popular programming languages, so it's not worth
people bothering to even try that methodology except if they're
going to publish the result in a scholarly ournal?)

I'm saying that most developers simply don't know how to proof
software. Testing is not proofing. Automatic proofing tools would
certainly help - but any possible tool is limited by the halting
problem and so there will always be code that the tool cannot prove
correct. And the tool would have to be simple enough for code-monkeys
to use and have warnings they could understand.

[Incidently, I'm not excepting myself. I *did* know how to write a
proof at one time, and even had to do so professionally for some
medical device software I once worked on. But I haven't done a
software proof in well over a decade and I doubt I could sit down and
do one now without methodology research.]


It's also the case that some popular programming languages have
features that impede easy analysis.

It's not necessary to *use* such difficult-to-analyze features, you
know?

Of course. However, a language with imperative features is inherently
more difficult to analyze than a language without them. The entire
point of some standard compiler transformations is to "functionalize"
the code and make it somewhat easier to analyze.

But even so, there are no "functional" CPUs ... all are imperative.
So, by rights, to prove the software, you have to prove both that the
source correctly implements the intent of the program under the
semantics of the source language, and also that the imperative
translation implements identical intent under the semantics of the
assembler language.

A good compilers is very hard to write - over the years I've been
involved with two projects.


If the parse tree for the software is readily available, as
it *is* for Lisp (and has been since the very start nearly fifty
years ago), it's possible to automatically analyze the software to
check what features it uses and warn if any difficult-to-analyze
feature is used, and not exactly where it's used. Then anyone
wishing to prove that the different individually-tested units can
be proven to work together, can attempt to modify the code (if
necessary) to eliminate use of any difficult-to-analyze feature,
and if successful then apply whatever multi-unit-analyzer software
is available. Have you investigated that idea to see how feasible
it might be? (Note that different features might cause difficulty
with different methods of multi-unit analysis, so a different
difficult-code detector might be needed for a different
multi-unit-analysis tool.)

With imperative languages, it's a lot harder than it sounds - there
are myriad special cases where a potentially unsafe construct is
suitably constrained and therefore not being used in a dangerous
manner. If you simply reported any use of the unsafe construct,
developers would start ignoring the warnings. You have to do a lot of
work to sort out what is dangerous from what looks like it might be
dangerous.


I think you'll agree that the vast majority of hardware designers
are content to pick parts out of catalogs rather than do materials
chemistry to build senary logic gates.

Back to that metaphor: Software is nearly *always* assembled from
low-level units that come from a catalog, namely the "Principles of
Operation" manual for the CPU when writing machine/assembly
language code, or the "API documentation" when writing code in a
higher-level language. For example, we have the Common Lisp
Hyper-Spec <http://www.isr.ist.utl.pt/library/docs/HyperSpec/Front/>
and the JavaDoc <http://java.sun.com/j2se/1.4.2/docs/api/index.html>
as "catalogs" of what API units are available for use (and
well-tested and believed to be working) in our application-level
software.

True, but not relevant. The discussion is about component (re)use of
off-the-shelf software by different authors, possibly written using
different languages.

Paul made an analogy to hardware, but to be similar, software
components must be in some immutable form that can be executed but not
modified by the developer.


Software developers, OTOH, do invent ad-hoc symbolism and
accompanying predicate systems every time they write a program

All within the framework provided by the API (or Principles of
Operation) manual. Nothing is invented do novo except *intentions*
of use of some existing type of data.


That is exactly what I'm talking about. The semantics of the platform
are not relevant. The program has its own symbology and semantics.
The hardware may see an integer value, say 42, but nothing constrains
the program to treat 42 as a number - it can be a symbol representing
anything that is meaningful to the problem domain.

The logic and semantics defined on the unique symbology of the program
is *always* ad-hoc.


Application programmers do *not* delve deep into the underlying
machine language to defeat the restrictions of the API, much less
modify the hardware to generate new machine language instructions
to take advantage of. So I believe here you're making much ado
about nothing.

It's only necessary to use data in a way that's inconsistent with its
nominal appearance. Like using 42 to mean

1 - open silo doors
0 - detach fuel line
1 - spin up gyros
0 - retract gantry
1 - start ignition
0 - deny recall


The problem of standardized software components will be solved as
soon as everyone can agree on a common paradigm neutral,
multi-language, cross-platform, immutable, type safe, modular
delivery system.

How about a syntax-free development and archival system, which
automatically lists which known programming languages support any
given module and offers a menu for converting the syntax-free
software to whichever of the known programming languages the user
wishes to express it in (port it to)? I've proposed this idea
several times recently, but nobody else has expressed any serious
interest.

I honestly have no idea what a "syntax-free" development system would
even look like. There is no such animal as a syntax free language and
back-translation from a language neutral IR to any particular high
level language more often than not produces garbage.

Java and .NET have the right idea - secure managed environments, a
common low level distribution format and compilation to native code at
load time (or alternatively at install time). It's the current
implementations of the idea(s) that are lacking.


Historically "warrant" was limited to the lifetime of the giver.
However, companies have (potentially) unlimited lifetimes.

Except that when a merge happens the new owner convenient forgets
any promises made by the previous company. For example, I opened an
account with Northern California Savings, because they had a
wonderful commercial on TV with a chain of dominos representing a
person's life time, which comes to an end at the end of the domino
chain, plus the fact they offered me free cheque printing for the
lifetime of the account. They were bought by Great Western Savings,
which honored the promise, which was later bought by Washington
Mutual which refused to honor the promise, started charging me for
cheque printing.

Those promises were not warrants (or guarantees) ... they were simply
corporate policies and as such were subject to change.

In many countries, an acquiring company must uphold obligations of the
acquired company. A warrant, however, is not an obligation or
responsibility - it is just an assumption of authority. The acquiring
company can choose not to assume authority over products or services
of the acquired company that they don't like. In that case the
orphaned products and services generally die unless someone else
assumes them.


Component software is a great idea but intractably hard in practice.

Do you mean that setting up formal specs for *all* the functions in
Common Lisp or *all* the classes/methods in Java etc. is
intractably hard (I would agree there), or that even doing formal
specs for a relatively well-behaved subset is intractably hard
(I might disagree with you if that's what you mean, but I'd need
to see you clearly state what you are saying before I post formal
rebuttal).

I mean exactly what I said previously. To recap: For software to be
componentized, it must become like IC hardware - an immutable
black-box deliverable which can only be executed according to its
specified interface. It must be impossible or at least unfeasibly
hard to tamper with the deliverable. It must be plug and play at
least on all the popular platforms and usable from any language or
development system that runs on those platforms.

That could be achieved now, but it would be nearly impossible to get
everyone to agree on an appropriate common delivery and management
system.


Honestly I can't care much about the lacking in Java's
documentation because Java as it exists now is not a suitable
candidate for a really useful componentized software platform.

Is any decent-sized subset of the Java 1.3 or 1.4 API suitable?

No.

Ignoring Java's deficiencies as a source language, the JVM is not a
good execution platform for languages whose features differ
significantly from Java. Advanced languages features not found in
Java can be implemented on the JVM with varying degrees of difficulty,
but their performance is frequently poor (see SISC for an example).
Sun, as yet, has shown no inclination to expand the JVM to accommodate
other languages. The delivery format is not externally tamper-proof
and reflection allows runtime discovery and manipulation of objects in
ways the designer did not intend.

The same is true of .NET although its VM makes a bit more of an effort
to accommodate languages that Microsoft doesn't promote - for example,
..NET (as of version 2) directly supports tail recursion.

COM and Corba are ok but components are not hardware neutral like
bytecode files nor are they immune to tampering.


Neither is .NET, or Corba, or COM or anything I've yet seen.

How about a subset of Common Lisp??

No. Lisp has no non-source external format for code. The whole point
of component software is to use it as is and prevent modifications
that might affect the reliability of the code.


George
--
for email reply remove "/" from address
.

Relevant Pages

  • Re: VMS
    ... because it was tailored to the platform rather than the language. ... > best machine architecture (PDP-11, VAX, Alpha) and the best software. ... the hardware really didn't matter. ... applications and in the IT world bus speed is more important than ALU ...
    (comp.object)
  • Re: a dozen cpus on a chip
    ... No nontrivial language can ever be proven to be imposible to crash. ... compilers still available which implement ISO M2. ... It is a common misconception that Lisp is always interpretted. ... various X86 machines the hardware does exist that could allow the OS ...
    (sci.electronics.design)
  • Re: How much intelligence?
    ... Curt believes in things that have hardware that enables them to talk. ... have the same language skills we have. ... These representations of reality are represented in long-term memory, ...
    (comp.ai.philosophy)
  • Re: Another transputer-inspired language?
    ... describe permanent ASIC/VLSI hardware devices. ... only support Verilog & VHDL. ... shrinking but the no of FPGA starts is exploding due to lowish NRE ... When I suggest the V++ language be modeled after ...
    (comp.sys.transputer)
  • Re: Intermediate forms (again?): worthwhile?
    ... writing to the hardware level for my language's ... your compiler will generate code close to the hardware? ... The implementation strategy depends on the features of your language. ...
    (comp.compilers)