[Info-vax] Opportunity for VSI?

[gérard Calliet]

Le 20/12/2018 à 11:00, johnwallace4 at yahoo.co.uk a écrit :
> On Thursday, 20 December 2018 00:40:52 UTC, Arne Vajhøj  wrote:
>> On 12/19/2018 3:09 PM, gérard Calliet wrote:
>>> Le 19/12/2018 à 20:43, Arne Vajhøj a écrit :
>>>> On 12/19/2018 2:39 PM, Bill Gunshannon wrote:
>>>>> On 12/19/18 2:25 PM, Arne Vajhøj wrote:
>>>>>> There are two schools of thought on programming languages.
>>>>>>
>>>>>> There are those that prioritize the power of the language - it
>>>>>> should be possible to express even very complex logic in a
>>>>>> short and concise way.
>>>>>>
>>>>>> And there are those that prioritize simplicity of the
>>>>>> language - it should be possible for anybody with an
>>>>>> IQ over 90 to read and understand the code.
>>>>>>
>>>>>> Ada95 and Scala definitely seems to be designed
>>>>>> by people in the first category.
>>>>>
>>>>> I don't know about that.  Ada w3as used as an introductory
>>>>> language at Universities and that was back when the average
>>>>> incoming student hadn't seen a computer more advanced than
>>>>> a TRS-80 or Apple ][.  They had no problem grasping it and
>>>>> by their second year were writing rather complex programs
>>>>> with it.
>>>>
>>>> Ada95 or Ada83 ?
>>
>>> Somethings very subtle can be used in Ada 83, 95, 2012 (2012 introduced
>>> the idea of contracts, first saw in Eiffel long time ago, and very
>>> powerfull), but I have to agree with Bill, Ada is also well structured
>>> and has been used on education, because, being not at all ambiguous it
>>> can be used to make believe students that programs have to do
>>> predictable actions :) , and using small simple parts of the langage is
>>> possible for all IQ :)
>>>
>>> Me best lesson in programming has been a year with first part in Caml
>>> (functional) "doing the most rational thing" said the teacher, and the
>>> second part in Ada "you can translate that to simpler procedural simple
>>> language" said her.
>>>
>>> The similarity between Scala and Ada, for me, and thought there are
>>> totally different way of programming, is that they suppose a scientific
>>> basis, and so it is possible to think programming more as a rational
>>> action than  a probalistic action.
>>>
>>> A subset of Ada, Spark, is used as a tool in formal proofs of programs.
>>> Which indicates Ada is in the universe of predictable programming.
>>
>> I know that the "use of a subset of Ada" approach is sometimes used
>> but I see that as an indication that the full language may be
>> too complex for some contexts.
>>
>> Arne
> 
> I wonder how many readers have come across things like SPARK Ada
> in any real detail, in places where they are a good fit?
> 
> 
> Here's a brief extract which may help shed more light, from
> https://www.embedded.com/electronics-blogs/other/4419245/SPARK--Why-I-am-backing-a-predictable-winner)
> 
> "The SPARK programming language, as described in previous postings was specifically designed with the goals of predictability and verifiability in mind. One of the key concepts embodied in SPARK is that of a contract: a statement of intended functionality by a designer which has to be met by the implementer and can be automatically checked by support tools.
> 
> As a result of their success in the field of program verification, contracts have now been absorbed into Ada - the mainstream language of which SPARK is a contractualised subset. Ada 2012 – the most recent version of the language – now contains a native syntax for functional contracts expressed as Pre and Post “Aspects.” Accordingly, the next generation of the SPARK language, called SPARK 2014 , will switch from using structured comments for contracts to using the built-in Ada 2012 equivalents. "
> [end of extract]
There is also a lot of interesting things about Spark and its uses done 
by Adacore for the Ada community, for example:
https://www.adacore.com/books/embedded-spark-and-ada-use-cases
> 
>  From my point of view, it's not just about subsetting to
> reduce the impact of language complexity. It's about
> testability and verifiability of design and runtime,
> and including this capability from day 1, in a productive
> way.
I agree, I was saying very little introduction. Thanks to all the 
complements you gave.
> 
> If someone can make any Ada program compile, there's a
> fair chance that its runtime behaviour will be as the
> coder intended.
> 
> If it's based on SPARK, with proper pre-conditions and
> post-conditions as well, it might even behave as the
> specifier and designer intended.
> 
> If the Ada in question is generated by some shiny "model-based
> systems engineering" tool, purely for "tick the box" compliance,
> and is the kind of Ada that no sane human would ever produce,
> then the language isn't really being used in the intended manner.
> 
> Same as the way CORAL 66 used to be abused for tick-the-box
> compliance - write the whole thing in the kind of inline
> assembler that was acceptable to the CORAL compilers of the day,
> and the purchasing departments and regulatory authorities seemed
> to be happy enough. Whether engineers would be so happy didn't
> seem to matter.
> 
> But a week or two of specification and design work up front can
> often be used to avoid months of test+debug time later, so
> where's the incentive (especially in a world of cost-plus
> contracts).
> 
> 
>