[ / / / / / / / / / / / / / ] [ dir / 1cc / asatru / asmr / roze / strek / sw / thestorm / vp ][Options][ watchlist ]

/tech/ - Technology

You can now write text to your AI-generated image at https://aiproto.com It is currently free to use for Proto members.
Name
Email
Subject
Comment *
File
Select/drop/paste files here
* = required field[▶ Show post options & limits]
Confused? See the FAQ.
Expand all images

[–]

 No.834604>>834610 [Watch Thread][Show All Posts]

Safe Pointers in SPARK 2014

RUSTLETS BTFO

In the context of deductive software verification, programs with pointers present a major challenge due to pointer aliasing. In this paper, we introduce pointers to SPARK, a well-defined subset of the Ada language, intended for formal verification of mission-critical software. Our solution is based on static alias analysis inspired by Rust's borrow-checker and affine types, and enforces the Concurrent Read, Exclusive Write principle. This analysis has been implemented in the GNAT Ada compiler and tested against a number of challenging examples including parts of real-life applications. Our tests show that only minor changes in the source code are required to fit the idiomatic Ada code into SPARK extended with pointers, which is a significant improvement upon the previous state of the art. The proposed extension has been approved by the Language Design Committee for SPARK for inclusion in a future version of SPARK, and is being discussed by the Ada Rapporteur Group for inclusion in the next version of Ada. In the report, we give a formal presentation of the analysis rules for a miniature version of SPARK and prove their soundness. We discuss the implementation and the case studies, and compare our solution with Rust.

https://arxiv.org/abs/1710.07047

https://arxiv.org/pdf/1710.07047.pdf

discuss

 No.834609

>Finally, we should note that our analysis does not require any additional user annotation to the source code (whereas Rust needs sometimes explicit lifetimes to be specified), and the rules are unambiguously defined whereas for Rust no official document specifies the borrow-checker (the README provided is quite incomplete).

Sick burn. This sentence alone BTFO Rust to infinity.


 No.834610

>>834604 (OP)

>discuss

This is just the Steve Klabnik LARPer baiting.

saged and reported


 No.834615

>This analysis has been implemented in the GNAT Ada compiler

when can I use it with open-source GNAT?


 No.834619>>834622 >>834623

>The first example is the swap procedure, whose naive implementation gets accepted by our rules. Note that there is no way of implementing a swap function in Rust.

<our rules do not handle as much features as Rust’s borrow-checker, but allows more constructs than Rust

<Initialization checks are similarly done by Rust’s borrow-checker in a safe way, whereas our rules only catch some uninitialized variable usage

<Nullity-checking is also a built-in feature of Rust (there a no safe null pointers in Rust), whereas we allow them,

<Another interesting design choice we made, is to ban borrows or observes inside a block, whereas Rust allows it.

excitement level: deflating


 No.834622>>834639

>>834619

>Note that there is no way of implementing a swap function in Rust.

what do they mean with swap? do they mean swapping the values of two pointers? if so this is possible in rust: https://doc.rust-lang.org/std/mem/fn.swap.html


 No.834623>>834625

>>834619

><Nullity-checking is also a built-in feature of Rust (there a no safe null pointers in Rust), whereas we allow them,

Does this matter? The worst thing you'd get from dereferencing a null pointer is an exception; rather than any real safety concerns.


 No.834625>>834628

>>834623

Actually in C/C++ dereferences a null pointer is UB. Only in pajeet langauages like Java/C#/etc. you are guaranteed to get an exception.


 No.834628

>>834625

I guess I was thinking about the OS itself, but I agree the compiler isn't guaranteed to try to address 0x0 in the application's address space.


 No.834639>>834649

>>834622

Only by circumventing the borrow checker. std::mem::swap uses unsafe pointer reads/writes.


 No.834649>>834651

>>834639

Nothing wrong with that.

Dear OP, what's great about Ada? Why would I want to learn that? I've never met anyone IRL talking about Ada, so it always seemed to me like some obscure special meme language that no one uses. Please tell.


 No.834651>>834652

>>834649

Why have a borrow checker in the first place when you have to circumvent it to do anything useful?


 No.834652>>839691

>>834651

>having disadvantages means it is all bad

Kill yourself anti Rust shill


 No.839691

>>834652

>>834652

>CY+3

>being pro Rust

<Shigdiggity




[Return][Go to top][Catalog][Screencap][Nerve Center][Cancer][Update] ( Scroll to new posts) ( Auto) 5
13 replies | 0 images | Page ?
[Post a Reply]
[ / / / / / / / / / / / / / ] [ dir / 1cc / asatru / asmr / roze / strek / sw / thestorm / vp ][ watchlist ]