Re: GNAT packages in Linux distributions

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

Le Fri, 04 Jun 2010 15:49:49 +0200, Georg Bauhaus  
<rm.dash-bauhaus@futureapps.de> a écrit:
> Coding invariables makes me think of a tricky(?) question:
> What should a language look like that naturally makes the programmer
> think before coding, and take his/her time?  What would its
> features and offerings have to be?
Undoubtedly, I would think to start with a VDM like (whose theory I know a  
bit, however never practiced, sorry)

I don't mean Ada is not nice for that (it has many things which suggest  
you to think about the logic and structure of things before to start, and  
SPARK completes it has it give logic), I just mean this has some  
additional things, which make it mandatory (based on what I read about it  
some 15 years ago).

Do you agree with that idea ?

My advocating: it starts with high level expressions [*], which are not  
even compilable (don't even think about such a word as “coding” in this  
context). Then you go down to implementation step by step, and each step  
has to be proved (the kind of proof it uses is comparable in some way to  
the ones of SPARK). There is no other road than, first, know what you want  
(very important), then, know why it can be implemented this/that way  
(requirement: intuitions, as with any logic/mathematical proof).

[*] Please, don't tell me UML do the same, although it may be nice for  
communication (another area).

> One inescapable ingredient of any popular PL seems to be magic at the
> level of syntax, if this is how programmers most visibly see themselves
> express themselves.  Can't force them to wear boring ties. Eiffel's
> syntax appears to be expanding ...
I did not understood this sentence: “Eiffel's syntax appears to be  
expanding ...”
What you were you to mean ?

> Maybe some Cobol style modules headers listing major internal
> and external parts to be manipulated might help?
Can you give a short example of what it would look like for ones who don't  
know COBOL ?


Are you to complete your list of thoughts about programming languages in  
the large ? (I remember  you talked about it if I'm not wrong)

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.