Software Assurance Reference Dataset

[Walter Bright via Digitalmars-d]

On 6/26/2014 2:01 PM, Araq wrote:
>>
>> Spark is a research language that does not work, as I've discovered and
>> discussed with you before. It cannot be determined the max stack usage at
>> compile time, again, this is the halting problem.
>>
>
> What?! It's easily solvable: Forbid recursion and indirect
> function calls

Oh well, there goes about 90% of D programs and pretty much all use of the D 
runtime library!


> and it's guaranteed that the program only requires
> a fixed size stack and you can compute an upper bound of the
> required stack size at compile-time. Which is BTW exactly what
> OpenCL does as GPUs tend to have no stacks.
>
> In what way is Spark a "research language that does not work"?

A while back, bearophile posted here some advocacy that Spark was using its 
contracts to prove things about the code. I experimented with it a bit and 
discovered that such proofs did not go beyond the trivial. As I recall, 
bearophile then agreed that it was a great idea that the implementation fell far 
short of.


 > And how many language design issues need to be discovered until
 > you admit that Safe-D is a "research language that does not work"?

I recommend that all such issues you discover be put on bugzilla, and marked 
with the 'safe' keyword, so they can be addressed.

I think there's a big difference between "only works for trivial cases" with no 
idea how to handle the rest and "does not work for all cases" and there being 
reasonable paths to handle them.

I admit that Safe D does not yet handle all the cases.