Comment by dandotway | Hacker News Reader

Comment by dandotway | Hacker News Reader

Parent Full thread

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