5 ms·

Seems AdaCore is working to add some form of borrow-checker to Spark :-) https://cps-vo.org/node/34575 https://cps-vo.org/node/34575

nickpsecurity 9y ago
I don't see anything about safety for dynamic, memory management in that link. It just talks about correctness. I'm specifically wanting affine types and ownership system that let SPARK go from static to dynamic. I do like them splitting it into several levels, though. That worked under Orange Book for security.
- pjmlp 9y ago
  AdaCore hired the guy that designed ParaSail, however the language development is a bit slow. https://forge.open-do.org/plugins/moinmoin/parasail/FrontPage https://forge.open-do.org/plugins/moinmoin/parasail/FrontPag...
  - nickpsecurity 9y ago
    In case you're interested in details on this development: https://news.ycombinator.com/item?id=14346032 https://news.ycombinator.com/item?id=14346032
- 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 :-).
nickpsecurity 9y ago
In case you're interested, here was a reply from Yannick at AdaCore: https://groups.google.com/d/msg/comp.lang.ada/H35QcYiWR1Y/jJNZ0tKqAAAJ https://groups.google.com/d/msg/comp.lang.ada/H35QcYiWR1Y/jJ... It seems they're adding a little bit of it for SPARK but not critical, dynamic part. I asked him at the end if they plan to go full, dynamic safety for full Ada if the SPARK experiment succeeds. Awaiting the reply.
- 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. One of the main limitations of the tech is 'no pointers' in SPARK mode. There are some tricks to hide pointers (you may want to look up the SPARK deployment guide : http://www.adacore.com/knowledge/technical-papers/implementation-guidance-spark/ http://www.adacore.com/knowledge/technical-papers/implementa... ) but it would allow so much more code to be SPARK-compatible. Even in the embedded space sometimes you need pointers and linked-lists and hashmaps (and the new formal containers don't do it for you)... Frama-C allows (and seems to work with) pointers, I don't know how Well. For Ada you can already go a long way (memory safety and data races) with protected object (nice semantics, check performance), not null pointers, controlled-types... But we're far from Rust's borrow-checker and move semantics. The name Unchecked_Deallocation (to instantiate 'Free') says it all. Can't wait to see some progress on this !

nickpsecurity 9y ago

I don't see anything about safety for dynamic, memory management in that link. It just talks about correctness. I'm specifically wanting affine types and ownership system that let SPARK go from static to dynamic. I do like them splitting it into several levels, though. That worked under Orange Book for security.

pjmlp 9y ago
AdaCore hired the guy that designed ParaSail, however the language development is a bit slow. https://forge.open-do.org/plugins/moinmoin/parasail/FrontPage https://forge.open-do.org/plugins/moinmoin/parasail/FrontPag...
- nickpsecurity 9y ago
  In case you're interested in details on this development: https://news.ycombinator.com/item?id=14346032 https://news.ycombinator.com/item?id=14346032
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 :-).

nickpsecurity 9y ago

In case you're interested, here was a reply from Yannick at AdaCore: https://groups.google.com/d/msg/comp.lang.ada/H35QcYiWR1Y/jJNZ0tKqAAAJ https://groups.google.com/d/msg/comp.lang.ada/H35QcYiWR1Y/jJ... It seems they're adding a little bit of it for SPARK but not critical, dynamic part. I asked him at the end if they plan to go full, dynamic safety for full Ada if the SPARK experiment succeeds. Awaiting the reply.

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. One of the main limitations of the tech is 'no pointers' in SPARK mode. There are some tricks to hide pointers (you may want to look up the SPARK deployment guide : http://www.adacore.com/knowledge/technical-papers/implementation-guidance-spark/ http://www.adacore.com/knowledge/technical-papers/implementa... ) but it would allow so much more code to be SPARK-compatible. Even in the embedded space sometimes you need pointers and linked-lists and hashmaps (and the new formal containers don't do it for you)... Frama-C allows (and seems to work with) pointers, I don't know how Well. For Ada you can already go a long way (memory safety and data races) with protected object (nice semantics, check performance), not null pointers, controlled-types... But we're far from Rust's borrow-checker and move semantics. The name Unchecked_Deallocation (to instantiate 'Free') says it all. Can't wait to see some progress on this !