GOPHERSPACE.DE - P H O X Y
gophering on hngopher.com
HN Gopher Feed (2017-12-07) - page 1 of 10
 
___________________________________________________________________
Safe Pointers in SPARK 2014
20 points by touisteur
https://arxiv.org/abs/1710.07047
___________________________________________________________________
 
[deleted]
 
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
safe languages!
 
  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
  work.
 
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
    here:https://www.adacore.com/books/safe-and-secure-
    softwareThrow in a good article on
    top:http://www.electronicdesign.com/embedded-
    revolution/assessin...
 
  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[0] in case anyone is interested.[0]:
http://archive.adaic.com/intro/tech/safe_ptr.html
 
  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.