Hacker News Reader

Comment by xavxav | Hacker News Reader

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) 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.

View on HN

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

That kind of software is not usually written in Rust (or Ada), but using Simulink / SCADE or other model-based and synchronous tools, afaik.

what are those tools written in?

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).

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.

> I'm curious what kinds of software they want to (eventually) verify,

https://www.reddit.com/r/rust/comments/sijixb/adacore_and_fe...

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.

Reply on news.ycombinator.com