Prev: simple: P versus NP
Next: 19990823: General announcements. Goedel's question: if a theorem has a proof of length at most n, can we find it in time O(n^2)? Another question on what can be computed in limited time and space.
From: Mok-Kong Shen on 28 Oct 2009 04:14
Pascal J. Bourguignon wrote:
> Tim Little wrote:
>
[snip]
> If you accept that big systems must be decomposed into small programs,
> you should probably also accept that big specifications are as bad as
> big program(*), and that they should be short too, to be
> understandable and effectively implementable. Then the degree of
> automatization in the process of translating the specifications into
> executable code is only a matter of advancement of the techniques,
> while the size of the executable code is only (roughly) a function of
> the number of metaprogramming levels used.

I barely know anything in this direction. But isn't it that UML
is supposed to be able to do stepwise refinement of design up
to the point of transition to executable codes? I saw long time
ago also a leaflet advertising a different commercial system
that claims to include even the code generation step.

M. K. Shen
From: Mok-Kong Shen on 28 Oct 2009 04:59
robertwessel2(a)yahoo.com wrote:
[snip]
> Yet we keep building bigger systems than we can do comfortably,
> because we want them to do more. The new Boeing 787 is reported to
> have 6.5 million lines of code in the various aircraft systems (not
> counting things like the passenger entertainment systems). And I can
> assure you that Boeing doesn't have any desire to take on a software
> project that big, but rather it's what they needed to do to accomplish
> their goals of building a next generation airliner ('course they're
> still working on that).
[snip]
> Good specifications are basically of similar difficulty to write as
> the actual code. This is the downfall of many formal methods - a
> specification complete enough that allows an automated checker of some
> sort to verify that the software implements the specification is
> basically as hard to write as the software. And as hard to verify
> that it's correct.

Verification seems to be an inherently unachievable goal. If one
uses a software to do verification, that software itself evidently
has to be verified. So I personally wonder how absolute correctness
could be achieved in practice at all. Anyway, a recent news said that
some 7000 lines of code of the kernel of an operating system has been
verified with a sophisticated verification system plus some 6 man years.

M. K. Shen
From: Joshua Cranmer on 28 Oct 2009 08:05
On 10/28/2009 12:32 AM, Pascal J. Bourguignon wrote:
> Can you not specify all programming problem in less that a few
> thousands of lines of specification?
>
> Well, you can always write more detailed specifications, but I can
> assure you that sales peoples will always be able to put the whole
> specifications of your software on a 2-page booklet.

The PDF 1.6 specification was, if I recall correctly, approximately 1400
pages of text. My draft of C++0 weighs in at a whopping 1314 pages. The
JVM spec is smaller, at only 542 pages. The full x86_64 ISA comes in
volumes; even the ancient MC6800 ISA took 40 pages or so to explain.

Many specifications, to approach the degree of completeness required for
independent implementation, need to drag on for hundreds or thousands of
pages.

--
Beware of bugs in the above code; I have only proved it correct, not
tried it. -- Donald E. Knuth
From: Pascal J. Bourguignon on 28 Oct 2009 11:38
Mok-Kong Shen <mok-kong.shen(a)t-online.de> writes:

> robertwessel2(a)yahoo.com wrote:
> [snip]
>> Yet we keep building bigger systems than we can do comfortably,
>> because we want them to do more. The new Boeing 787 is reported to
>> have 6.5 million lines of code in the various aircraft systems (not
>> counting things like the passenger entertainment systems). And I can
>> assure you that Boeing doesn't have any desire to take on a software
>> project that big, but rather it's what they needed to do to accomplish
>> their goals of building a next generation airliner ('course they're
>> still working on that).
> [snip]
>> Good specifications are basically of similar difficulty to write as
>> the actual code. This is the downfall of many formal methods - a
>> specification complete enough that allows an automated checker of some
>> sort to verify that the software implements the specification is
>> basically as hard to write as the software. And as hard to verify
>> that it's correct.
>
> Verification seems to be an inherently unachievable goal. If one
> uses a software to do verification, that software itself evidently
> has to be verified.

Happily, the verification software may be simplier than the verified
software. Therefore it should be easier to verify. Possibly by a
second order verification software that is itself even simplier to
verify. And so on, until you can have it verified it by hand by as
many human you need to reach the required degree of confidence.


> So I personally wonder how absolute correctness
> could be achieved in practice at all. Anyway, a recent news said that
> some 7000 lines of code of the kernel of an operating system has been
> verified with a sophisticated verification system plus some 6 man years.
>
> M. K. Shen

--
__Pascal Bourguignon__
From: Pascal J. Bourguignon on 28 Oct 2009 11:43
Mok-Kong Shen <mok-kong.shen(a)t-online.de> writes:

> Pascal J. Bourguignon wrote:
>> Tim Little wrote:
>>
> [snip]
>> If you accept that big systems must be decomposed into small programs,
>> you should probably also accept that big specifications are as bad as
>> big program(*), and that they should be short too, to be
>> understandable and effectively implementable. Then the degree of
>> automatization in the process of translating the specifications into
>> executable code is only a matter of advancement of the techniques,
>> while the size of the executable code is only (roughly) a function of
>> the number of metaprogramming levels used.
>
> I barely know anything in this direction. But isn't it that UML
> is supposed to be able to do stepwise refinement of design up
> to the point of transition to executable codes? I saw long time
> ago also a leaflet advertising a different commercial system
> that claims to include even the code generation step.

All the techniques developed so far are only one step techniques.
Useless.

What we really need is metaprogramming. The only usable
metaprogramming solution I know is Lisp and its macros. With
metaprogramming, you can implement as many steps you need to keep the
complexity in check.


--
__Pascal Bourguignon__
First  |  Prev  |  Next  |  Last
Pages: 1 2 3 4 5 6 7 8 9 10 11 12
Prev: simple: P versus NP
Next: 19990823: General announcements. Goedel's question: if a theorem has a proof of length at most n, can we find it in time O(n^2)? Another question on what can be computed in limited time and space.