HN Gopher Feed (2017-12-07) - page 1 of 10
Safe Pointers in SPARK 2014
20 points by touisteurhttps://arxiv.org/abs/1710.07047
stmw - 48 minutes ago
You know Rust is gaining traction when people are writing papers
discussing adding Rust borrow-checker features to an Ada-inspired
pjmlp - 35 minutes ago
The biggest impact was definitely to make more approachable the
design of ATS and Cyclone to common developers.But borrow-checker
still needs some fine tuning, as per NLL and further planned
silverlake - 44 minutes ago
Why don?t more people use SPARK?
MisterTea - 42 minutes ago
Why don't more people use Ada?
yeukhon - 16 minutes ago
Ada is quite common in aircraft system programming.P.S. I
thought I read SPARC.
nickpsecurity - 28 minutes ago
Anyone curious of its benefits can find them
softwareThrow in a good article on
th0br0 - 40 minutes ago
Because of licensing?
pjmlp - 37 minutes ago
I guess, because GNAT is the only free Ada compiler, all the
remaining ones being commercial.So Ada and SPARK ended up just
catering to the industry that created them, high integrity
systems, the kind where people die when an out-of-bounds occurs.
digikata - 21 minutes ago
I've always wondered if it was in part because porting an ADA
compiler ideally also involves porting some support for
constructs like TASK - which ends up more like getting
maintenance in place for both a language compiler as well as OS
elements. In comparison porting a C compiler is mostly about
the instruction set, and you can separately decide to
port/support thread libs or selected RTOSes.It's been a long
time since I programmed in ADA, but the TASK support on the
toolchain/system I was a long time ago sucked, and you couldn't
climb into it and fix it like you might a standalone C RTOS
because it was part of the tooling supplied by a vendor.Vs with
Rust, the borrow checker is fairly portable memory lifetime
tracking and reasonably independent of hw architectures.
kuwze - 43 minutes ago
There is also safe_ptr in case anyone is interested.:
pjmlp - 33 minutes ago
Thanks, quite interesting, specially the publication year (1999),
yet another proof how long people have been trying to advocate
for safer systems.
nickpsecurity - 31 minutes ago
I told Yannick at AdaCore that getting parity with Rust's borrow-
checker was critical given SPARK was otherwise the champ of highly-
assured, system code. He said someone was working on something like
that. I appreciate the tip from touisteur about this work because
it's awesome!This is also potentially a boost for my Brute-Force
Assurance concept of doing versions of same code in multiple
languages to leverage their verification tooling, esp automated.
One obstacle was mismatch between Rust's pointers with borrow-
checker and SPARK's lack of them. Bringing them closer together
might let one use SPARK to model unsafe code in Rust to prove its
safety. Other languages, too.