30 Sept 2024 17:17:13 nick <nick@???>:

> It is called Spark. I haven't tried Spark or Ada but I think it could well be worth a look.

Robert Dewar once said that Ada has better support for pointer arithmetic than C.

Of course it isn't needed and best avoided in Ada. There are far better options.

Spark is a proving tool that understands the flow of an Ada program at compile time. It is more capable than Rust and the good thing about it being a separate tool is that this proving does not impact compilation time. The Gnat compiler still sees if you have specified that some code or a whole package is in spark mode and will give an error if you use a feature such as dynamic oop that isn't allowed in spark due to it breaking the ability to perform compile time flow analysis.

Spark actually supports borrowing now and even prevents memory leaks (rust doesn't). I think it is much neater than Rusts borrowing. You can see that demonstrated here.

https://youtu.be/97G1V2U8Drk?si=o5AL5OpoLVlMHwS1