> I would prefer sometimes consistency: for gnatstack to support at least the SPARK subset (so, OOP, access to procedures, most 'reasonable' provable language f

> I would prefer sometimes consistency: for gnatstack to support at least the SPARK subset (so, OOP, access to procedures, most 'reasonable' provable language features) Again though this would require some way of enabling SPARK to track the stack-depth guarantees of every possible function that might be executed. Not to say it would be impossible, but I imagine it's far simpler for GNATstack to simply 'ban' function-pointers and dynamic dispatch. > it's happened to me, on AoRTE (silver-level) SPARK, to crash because of an overeager parser To be clear then this was deep recursion in a parser blowing the stack? Honestly I'm a little surprised SPARK even permits recursion in the first place. Seems like the 'safer' thing to do would be to forbid recursion and force the programmer to manually manage a stack data-structure (presumably one of fixed size). > I'm guessing it's mostly 'no-one put a wad of cash thick enough on the table to have another look' which is understandable I'm sure AdaCore are plenty motivated, but yes, no doubt they have only limited resources.