Beingessner: Rust's Unsafe Pointer Types Need An Overhaul [LWN.net]

Beingessner: Rust's Unsafe Pointer Types Need An Overhaul

Posted Mar 23, 2022 23:01 UTC (Wed) by Cyberax (✭ supporter ✭, #52523)
In reply to: Beingessner: Rust's Unsafe Pointer Types Need An Overhaul by acarno
Parent article: Beingessner: Rust's Unsafe Pointer Types Need An Overhaul

The last time I looked at Ada, it seemed like pointers ("access types") were an afterthought there. Is there a good documentation about something like borrow checker but for Ada?

to post comments

Beingessner: Rust's Unsafe Pointer Types Need An Overhaul

Posted Mar 25, 2022 16:58 UTC (Fri) by mathstuf (subscriber, #69389) [Link] (2 responses)

There's some Ada proof assistant-like project named SPARK that I read an article about the beginnings of Rust' borrow checker influencing its design or progress. I may be mis-remembering details as to what SPARK is or how influential Rust has been on it.

https://blog.adacore.com/using-pointers-in-spark

Beingessner: Rust's Unsafe Pointer Types Need An Overhaul

Posted Mar 25, 2022 19:12 UTC (Fri) by Cyberax (✭ supporter ✭, #52523) [Link] (1 responses)

I admittedly hasn't looked into SPARK within the last 5 years, but way back then it didn't support non-static allocations. It was actually a "feature" there - bounded resource usage (because it can't be dynamic).

Beingessner: Rust's Unsafe Pointer Types Need An Overhaul

Posted Mar 25, 2022 19:55 UTC (Fri) by ms_43 (subscriber, #99293) [Link]

See this FOSDEM 2021 talk by Claire Dross:

Proving heap-manipulating programs with SPARK
The SPARK open-source proof tool for Ada now supports verifying pointer-based algorithms thanks to an ownership policy inspired by Rust

https://archive.fosdem.org/2021/schedule/event/safety_ope...