Re: Some exciting new trends in concurrency and software design

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Thu, 23 Jun 2011 12:57:49 +0200, Yannick Duch�ne (Hibou57) wrote:

> Ignoring things can help.
> 
> There is always some stage where you ignore some one of some other things.

Yes, but you should not forget that you deal with a model. Many approaches
claiming themselves mathematically puristic suffer this error.

> FP is less executable than Ada, so there are things you will less bother  
> with FP, you will be required to bother about with Ada.

Do you mean that FP programs are never intended to be executed? (:-))

> Do you see what I mean ?

No, I suppose you mean that FPL are more declarative than Ada. That is not
necessarily true, because Ada as a language supporting OO decomposition has
much declarative stuff to support this, missing in the languages oriented
on procedural decomposition.

> By the way, if you want to prove an Ada program, how do you do it, if not  
> by turning it into a view where it is all made of expressions (with  
> possibly multiple expressions at some point, for coverage) ?

Again, if you mean that any formal proof has to be strictly declarative
(assuming its relation to the run time). Yes it evidently has to be. But
the proof is not the program itself. They are written in different
languages of different power. IMO, it is fundamentally impossible to melt
them into one.

Also consider what would happen if you wanted to prove the proof. You would
need a third language for which the second one would be "executable," and
the inference it does would be just a program.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de