Re: Problems with SPARK 2015 and XMLAda

[Shark8 <onewingedshark@gmail.com>]

On Thursday, August 20, 2015 at 2:36:09 PM UTC-6, Randy Brukardt wrote:
> "Shark8" wrote in message 
> news:9d3dc132-4e1a-4e9c-bcd4-82a42a73745f...
> ...
> > As others have said, SPARK is about avoiding exceptions completely 
> > (because
> > the relevant properties are proved) and therefore having exceptions in 
> > your SPARK
> >  code is not allowed.
> 
> One use of exceptions is to signal errors with the parameters of a 
> routine -- essentially the failure of a precondition. Clearly, it is better 
> that such things are proved impossible, and thus such exceptions are not 
> needed in SPARK.

This sort of exception is what I was thinking of.

> 
> But another use of exceptions is to signal things that cannot be known at 
> compile time. How can you tell in advance whether the file Foobar.Txt exists 
> on your disk? Even a pretesting it is unreliable (it could be deleted 
> between the test and the usage); one has to report the error at runtime.
> 
> SPARK forces such errors to be reported as error codes, and that's pure 
> evil. The problems with using error codes rather than exceptions to report 
> unlikely but possible errors are well-known, and forcing one to use that is 
> essentially junking decades of programming experience.

I *really* despise error-codes -- Though with Ada you can make it a bit nicer by having an actual enumeration, throwing the function-call into a case-statement, and letting the compiler smack you when you forget to cover one of the codes.

> 
> The lack of access types is similar; one has to emulate them using arrays in 
> SPARK, which is a 1950s programming technique. It's the sort of thing that 
> one uses Ada to get way from.

Yes, it is.
I wasn't aware of this 'feature' of SPARK.

> 
> At least the SPARK team is aware of these limitations and considering ways 
> to mitigate them in future versions of SPARK. What I hate is people spinning 
> these as "features" rather than just a limitation of prover technology (and 
> to me, an indication that SPARK tries to do too much).

I am hoping the SPARK team fixes some of those and it looks like they have been doing so -- just look at type-predicates: http://www.spark-2014.org/entries/detail/spark-2014-rationale-type-predicates