Re: GNAT packages in Linux distributions

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

Le Tue, 11 May 2010 19:08:16 +0200, <stefan-lucks@see-the.signature> a  
écrit:
> I am curious. Would you be willing to share some of your experience and
> tell us about the advantages and disadvantages of both approaches?
>
> Stefan
Well, as noted above, Eiffel is far more popular than SPARK, and there is  
a reason for that : as Eiffel is runtime oriented, it is less strict than  
SPARK, which is static analysis oriented.

Let say there is the same differences between SPARK and Eiffel than the  
ones you may have between typed and non-typed language.

A non-type language does not require you to validate any thing until  
runtime, and runtime (and to reach a specific branch, which is important  
to note) to raise an error (providing it is as least able to raise an  
error in such circumstance).

The same comment apply with SPARK vs Eiffel : Eiffel allow you to run a  
program without any other requirement, it just interpret the pre- and  
post- and invariant conditions you've written (Yes, although it is a  
compiled language, this features of Design by Contract are still  
interpreted in Eiffel, just like pragma Assertion are in Ada by the way).

Hey... you know, untyped language seems far easier at first glance : you  
write, you run, it crash... you modify some this-and-that, you run  
again... it don't crash (I mean you don't when and why it will crash the  
next time, which may wait for some weeks, months or year, who know ...)

Just think about the amount of time you may spent before making a program  
proof with SPARK, and compare that to the Eiffel way, where you will never  
know your implementation is wrong (so you will not have reason to be  
disappointed, although things are still wrong what ever is your feeling  
about it).

If you want to enjoy your language, Eiffel is probably the best.

... hmmmm.... after some though, this may depends on what to “enjoy”  
requires to you ; so the above sentence may or may not be true finally.

Seriously, given two languages, one which allow you to run you application  
the sooner, which one do you think many body will prefer ? ;)

Guess what is most famous and popular : JavaScript or Ada ?

I think this draw the big line.

TBH, there is also some important restriction which SPARK applies to what  
you may use with Ada : you will not be allowed to use generics and  
polymorphic dispatching as two examples. Why ? Just because SPARK cannot  
make some proof based on these materials. So is SPARK useful for more  
complex application. The answer is Yes, as you are not required to  
validate all of your application with SPARK, and you can validate some  
part of it. Think about SPARK as a step above typing. Typing just make  
proofs on components of your application, not on the application. SPARK  
may be used the same way, to make proofs on some component as well... and  
it is able to make proofs which cannot be expressed with type definitions.

-- 
pragma Asset ? Is that true ? Waaww... great