Re: Some exciting new trends in concurrency and software design

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Thu, 23 Jun 2011 12:25:00 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:
> This is a weak argument. The strong one is that the mathematical numbers
> used in engineering are simply incomputable. The question is not  
> efficiency
> ("how"), it is "if": you cannot represent numbers involved, e.g. real
> numbers. Engineering computations are on the model numbers, where range  
> is
> just one constraint among others.
Was indeed what I wanted to mean (yes, even SML is not able to really  
express the ideal nature of numbers, and nothing is able to).

> All programming is actually about constraints, which makes things so  
> hard,
> mathematically, algorithmically and also in terms of types (e.g. LSP
> violation). Ignoring this does not help.
Ignoring things can help.

There is always some stage where you ignore some one of some other things.  
This is an unavoidable part of a design or understanding process (either  
with math or computation, this is true with both). The question is: how do  
you forget less and less as the time go, and how do you ensure you do not  
forget what is relevant for this and that (“this” and “that” don't occur  
at the same time). That's why I underlined the matter of focus: Ada and  
SML have different focus.

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. There may be  
techniques to make FP more executable (I do not know enough about OCaml  
compilers), but I believe FP is primarily a seed to derive from. If you  
don't expect FP text to be a final release, you can drop some physical  
matters at this stage. Let say, if you can execute it, that's for testing  
and prove by execution, which make it more handy than maths.

Do you see what I mean ?

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) ? That's what  
SPARK do so far. Yes, SPARK include Ada's type constraint in the proof  
requirement, so that is not strictly comparable, but this is a matter of  
stage and focus. Let say the functional view you get when proving an Ada  
program with SPARK, is more frozen and narrowed than what an expression of  
the same program would be with SML. And “frozen” and “narrowed” should not  
occurs too much early (and can't occur early anyway), and even, you may  
want to keep an hand or an eye on the non-frozen / non-narrowed view at  
any time.

Do you feel the picture ?

-- 
“Syntactic sugar causes cancer of the semi-colons.”  [Epigrams on  
Programming — Alan J. — P. Yale University]
“Structured Programming supports the law of the excluded muddle.” [Idem]
Java: Write once, Never revisit