3 ms·

This is exciting! I've met with people from AdaCore and Ferrous systems (individually) several times and they're all serious, competent and motivated. I'm curi

by xavxav 5y ago

This is exciting! I've met with people from AdaCore and Ferrous systems (individually) several times and they're all serious, competent and motivated. I'm curious what kinds of software they want to (eventually) verify, my PhD thesis is developing a verification tool for Rust (https://github.com/xldenis/creusot https://github.com/xldenis/creusot) and I'm always on the look out for case studies to push me forward. The road to formally verified Rust is still long but in my unbiased opinion looking quite bright, especially compared to other languages like C. Ownership typing really, really simplifies verification.

bovermyer 5y ago
Verifying software used to control rocket fueling systems sounds like a good idea to me.
- xavxav 5y ago
  That kind of software is not usually written in Rust (or Ada), but using Simulink / SCADE or other model-based and synchronous tools, afaik.
  - gameswithgo 5y ago
    what are those tools written in?
    - fgh 5y ago
      This is a guess, but Simulink is most likely based on a mixture of C, C++ and Java (if we leave out MATLAB as an intermediate step).
  - bluGill 5y ago
    In large part because those models are easy to formally verify. I've become interested in SPARK of the past few years, but people tell me while you can verify it, it is hard to do right. (I have no idea) I don't work with them myself, but some of my coworkers do low level control of similar hardware and they mostly work in matlab for that reason. Well for new code, there is still a lot of C from 20+ years ago in production, it isn't formally verified but years of real world experience says it is pretty good. Everytime there is a new feature there is a decision to rewrite the whole in matlab, put in shims to write the new part in matlab, or just add the C.
steveklabnik 5y ago
> I'm curious what kinds of software they want to (eventually) verify, https://www.reddit.com/r/rust/comments/sijixb/adacore_and_ferrous_systems_joining_forces_to/hva9scj/ https://www.reddit.com/r/rust/comments/sijixb/adacore_and_fe...
- xavxav 5y ago
  Yea, I think that they're taking the correct approach. For certification reasons formal verification is not necessary or even really desirable, but a core hypothesis in my thesis is that we can lower the exponential factor of formal methods for Rust compared to C. The type system of Rust really helps simplify the work and I hope that Rust can be one the the languages that finally takes FV/FM 'mainstream' (it'll never be an average tool but less niche/expert). To that end I'm always on the lookout for moderate length program components (100-1kloc) with clear safety properties that need to be verified. The standard fare is datastructures, but I'd love to see if we can expand the applications.

by xavxav 5y ago

bovermyer 5y ago

Verifying software used to control rocket fueling systems sounds like a good idea to me.

xavxav 5y ago
That kind of software is not usually written in Rust (or Ada), but using Simulink / SCADE or other model-based and synchronous tools, afaik.
- gameswithgo 5y ago
  what are those tools written in?
  - fgh 5y ago
    This is a guess, but Simulink is most likely based on a mixture of C, C++ and Java (if we leave out MATLAB as an intermediate step).
- bluGill 5y ago
  In large part because those models are easy to formally verify. I've become interested in SPARK of the past few years, but people tell me while you can verify it, it is hard to do right. (I have no idea) I don't work with them myself, but some of my coworkers do low level control of similar hardware and they mostly work in matlab for that reason. Well for new code, there is still a lot of C from 20+ years ago in production, it isn't formally verified but years of real world experience says it is pretty good. Everytime there is a new feature there is a decision to rewrite the whole in matlab, put in shims to write the new part in matlab, or just add the C.

steveklabnik 5y ago

> I'm curious what kinds of software they want to (eventually) verify, https://www.reddit.com/r/rust/comments/sijixb/adacore_and_ferrous_systems_joining_forces_to/hva9scj/ https://www.reddit.com/r/rust/comments/sijixb/adacore_and_fe...

xavxav 5y ago
Yea, I think that they're taking the correct approach. For certification reasons formal verification is not necessary or even really desirable, but a core hypothesis in my thesis is that we can lower the exponential factor of formal methods for Rust compared to C. The type system of Rust really helps simplify the work and I hope that Rust can be one the the languages that finally takes FV/FM 'mainstream' (it'll never be an average tool but less niche/expert). To that end I'm always on the lookout for moderate length program components (100-1kloc) with clear safety properties that need to be verified. The standard fare is datastructures, but I'd love to see if we can expand the applications.