Comment by touisteur | Hacker News Reader

Comment by touisteur | Hacker News Reader

Parent Full thread

Strange (but interesting (point of view. I always found Frama-C so verbose where spark has most checks as implicit, and has ways to express not-null pointer as types. I've always found eacsl a pain to write and even more with pointer manipulation.

Spark has added checks on memory ownership, that it seems (willing to be corrected) Frama-C didn't have yet.

From a pure tech stack point of view, down there you'll find Why3 and SMT solvers to perform most automatic proof/discharging of verification conditions, and then around that you'll find either a rich set of plugins (Frama-C) because C is... a tall order, or a series of static analysis tools (heavy-duty like codepeer, or lightweight libadalang-based abstract interpretation things) combined into the proof and verification environment. There's also been a lot of amazing work on floating point code verification for both in the previous years, and it was done mostly at the Why3 and SMT solver (or different kind of solvers/verifiers such as gappa) so everyone profits.

And, lest people might think both communities don't interact, the Spark and Frama-C people have an annual (or is it every other year) joint conference.

I'd be quite happy to find more people diving into Frama-C and see what they do and how they manage to write safe software. I'd also be quite happy to see rust building over Why3 (among other things) for their proof/verification efforts. More fruits from all the deep efforts of the verification community.

Responding to each point you raised:

'Frama-C so verbose': ??? Ada is the most verbose programming language, ever, even before you had the extremely verbose Spark contracts. Could you show me an example of Frama-C with annotations being more verbose than Ada/Spark?

'Spark has added checks on memory ownership': A Rust-like pointer ownership tester has its advantages and limitations.

Advantages: if you have team of 20 engineers working on a 20 million line web browser and no single engineer understands how the whole code base works, a pointer borrow-checker prevents an important class of errors.

Disadvantages: Rust tutorials point out that you have to resort to 'unsafe Rust' to implement even an intro-to-computer-science linked list. You have to use unsafe Rust to implement your fancy heap manipulation algorithms. Unsafe vs safe Rust is a bit like Ada vs. Spark ("safe Ada").

'I'd be quite happy to find more people diving into Frama-C': Frama-C is trending upward and Ada is in decline, ever since the Ariane 5 explosion on 4 June 1996. The US DOD consequently shut down its Ada office and eliminated the Ada requirement, and C/C++ subsets increasingly dominated.

The verbosity I felt in Frama-C contracts (when I tried back when) e.g. was around C's lack of 'parameter passing intent' specification (Ada has in, out, in out, not just by-value, by-ref, by-constant-ref-but-have-fun-with-the-value. People pass their structures as reference (struct thing *) and you have to ensure everywhere that that pointer isn't null. Same for over/underflow that isn't implicit in C. So lots of things needed to be required/checked explicitly instead of implicitly of with typing in SPARK. Cbmc has a similar thing where it has options to insert check if you ask it, checks that cbmc decides where to put, but are not defined in the language.

As for the rest, I checked again some recent Frama-C examples after your reply and verbosity is on par (similar quantifiers, loop invariants, etc.) and I don't see 'extremely verbose' in neither. Mostly I was focused on implicit versus explicit (in a 'boilerplate' sense).

As for the decline of Ada I see different things in my industry and a language and environment that keeps evolving and getting into more industries and making strides in very interesting domains. The DOD isn't the most interesting indicator of the liveness of a language, and I'm not sure what Ariane 5 brings here, except that when you reuse a binary component in a different setting without integration testing you get wild French fireworks?

As for the 'can't program a basic list in rust' I can only say that 99.9% of the time we're not rewriting a basic data structure, we reuse one from some standard library or a trusted component library, and I may have seen maybe one bug in those in my 15y or sw engineering, and countless ones in app or business logic, or serialization/deserialisation code... So yeah, if rust, spark or other hard ass static analysis tools makers are reading this, please keep making proof & verification tech modular. The more the tech advances the more spark we can have proved automatically without proof chops, the safer the world will be. But let me opt in the very hard stuff, please... Let me put the effort where it counts.

Reply on news.ycombinator.com