touisteur

101 ms·

1291.
by touisteur 9y ago
Not as much as rust, but still. I'm not sure whether it qualifies as memory safety for you but using Controlled types alleviates a large part of the problems of dynamic memory allocation. http://www.adacore.com/knowledg
1292.
by touisteur 9y ago
Hey thanks for the pointer to this thread. Allowing pointers in SPARK would be incredible... Today SPARK is so interesting because it's not all-or-nothing. So some parts can be SPARK (with different levels of proof), others Ada, etc. O
1293.
by touisteur 9y ago
Well the argument seems to be that it's easier to hire 'experienced' java developers (hear: have 'java' on their resume...). But the people you get are for the most part either inexperienced (fresh out of school) or
1294.
by touisteur 9y ago
My bad, slides are not available yet... There's a mention in there about some rust-like ownership proof mechanism in their roadmap. I thought about our last exchange on SPARK & rust when I saw this :-).
1295.
by touisteur 9y ago
Well it all depends how 'hard' your real-time is. If you go with Atego/aonix, you can get down to almost-C-Ada-like latencies but be ready to change your java coding style. Sliced-time GC works OK until you put too much pres
1296.
by touisteur 9y ago
Seems AdaCore is working to add some form of borrow-checker to Spark :-) https://cps-vo.org/node/34575
1297.
by touisteur 10y ago
Well then you're going to be happy : there's a new Spark-to-C compiler. http://blog.adacore.com/spark-tetris-on-the-arduboy Maybe that's the one you're thinking about ? Also, I heard Rod Chapman (at the
1298.
by touisteur 10y ago
Thanks for the paper. It's indeed a game-changer to be able to mix Ada2012, Spark, and C in an industry-grade programming environment. You can gradually convert a legacy codebase. I've been replacing some crufty C parts with Ada-w
1299.
by touisteur 10y ago
SPARK is indeed very adapted to some kinds of code (protocols, serialization, deserialization, index manipulation, masks...). Proving the absence of runtime errors in such code is easy (not much help needed for the provers, just type your d