Hacker News Reader

Comment by imglorp | Hacker News Reader

The author indicates some obvious differences, including the fact that Ada has a formal spec and rust doesn't -- rustc seems to be both in flux as well as the reference implementation. This might matter if you're writing a new compiler or analyzer.

But the most obvious difference, and maybe most important to a user, was left unstated: the adoption and ecosystem such as tooling, libraries, and community.

Ada may have a storied success history in aerospace and life safety, etc, and it might have an okay standard lib which is fine for AOC problems and maybe embedded bit poking cases in which case it makes sense to compare to Rust. But if you're going to sit down for a real world project, ie distributed system or OS component, interfacing with modern data formats, protocols, IDEs, people, etc is going to influence your choice on day one.

View on HN

Rust has now a donated spec that was provided by Ferrocene. This spec style was influenced by the Ada spec. It is available publicly now on https://rust-lang.github.io/fls/ .

This is part of the effort of Ferrocene to provide a safety certificate compiler. And they are already available now.

This is only meaningful if Rust compiler devs give any guarantees about never breaking the spec and always being able to compile code that adheres to this spec.

Why so?

Specs for other languages are also for a specific version/snapshot.

It's also a specific version of a compiler that gets certified, not a compiler in perpetuity, no matter what language.

That's not how it works for most language standards, though. Most language standards are prescriptive, while Rust is descriptive.

Usually the standard comes first, compiler vendors implement it, and between releases of the spec the language is fixed. Using Ada as an example, there was Ada 95 and Ada 2003, but between 95 and 2003 there was only Ada 95. There was no in-progress version, the compiler vendors weren't making changes to the language, and an Ada95 compiler today compiles the same language as an Ada95 compiler 30 years ago.

Looking at the changelog for the Rust spec (https://rust-lang.github.io/fls/changelog.html), it's just the changelog of the language as each compiler verion is released, and there doesn't seem to be any intention of supporting previous versions. Would there be any point in an alternative compiler implementing "1.77.0" of the Rust spec?

And the alternative compiler implementation can't start implementing a compiler for version n+1 of the spec until that version of rustc is released because "the spec" is just "whatever rustc does", making the spec kind of pointless.

> Usually the standard comes first, compiler vendors implement it, and between releases of the spec the language is fixed.

This is not how C or C++ were standardized, nor most computer standards in the first place. Usually, vendors implement something, and then they come together to agree upon a standard second.

When updating standards, sometimes things are put in the standard before any implementations, but that's generally considered an antipattern for larger designs. You want real-world evaluation of the usefulness of something before it's been standardized.

Because otherwise the spec is just words on a paper, and the standard is just "whatever the compiler does is what it supposed to do". The spec codifies the intentions of the creators separately from the implementation.

In rust, there is currently only one compiler so it seems like there's no problem

There being only one compiler is exactly the problem.

How is this different from the existing situation that Rust remains compatible since Rust 1.0 over a decade ago?

Rust doesn’t have quite as strong compatibility guarantees. For example, it’s not considered a NC-breaking change to add new methods to standard library types, even though this can make method resolution ambiguous for programs that had their own definitions of methods with the same name. A C++ implementation claiming to support C++11 wouldn’t do that, they’d use ifdefs to gate off the new declarations when compiling in C++11 mode.

That's a good point about the #ifdefs thanks.

Too late to edit but I meant BC not NC

Thanks, that was easily the most confusing thing and I was like well... I understand everything else, if it's very important what exactly "NC-breaking" means I'm sure I will realise later.

By that criteria there's no meaningful C++ compiler/spec.

How so? There are compiler-agnostic C++ specs, and compiler devs try to be compatible with it.

What the GP is suggesting is that the rust compiler should be written and then a spec should be codified after the fact (I guess just for fun?).

> compiler devs try to be compatible with it.

You have to squint fairly hard to get here for any of the major C++ compilers.

I guess maybe someone like Sean Baxter will know the extent to which, in theory, you can discern the guts of C++ by reading the ISO document (or, more practically, the freely available PDF drafts, essentially nobody reads the actual document, no not even Microsoft bothers to spend $$$ to buy an essentially identical PDF)

My guess would be that it's at least helpful, but nowhere close to enough.

And that's ignoring the fact that the popular implementations do not implement any particular ISO standard, in each case their target is just C++ in some more general sense, they might offer "version" switches, but they explicitly do not promise to implement the actual versions of the ISO C++ programming language standard denoted by those versions.

Neither the Rust nor the Ada spec is formal, in the sense of consumable by a theorem prover. AFAIK for Ada Spark, there is of course assumptions on the language semantics built-in to Spark, but: these are nowhere coherently written down in a truly formal (as in machine-readable) spec.

There was also Larch/Ada [0], which was a formally proved subset of Ada, developed for NASA [1].

[0] https://apps.dtic.mil/sti/tr/pdf/ADA249418.pdf

[1] https://ntrs.nasa.gov/citations/19960000030

What even is the most complex programming language with a fully machine-checkable spec? Are there actually practically useful ones? I know of none.

One candidate is ATS [1].

Another, https://cakeml.org/

[1]: https://en.wikipedia.org/wiki/ATS_(programming_language)

For the seL4 proofs a subset of C was formalized, for example.

(Already mentioned) CakeML would be another example, together maybe with its Pancake sibling.

Also: WebAssembly!

There's a formally verified C compiler, IIRC the frontend isn't, but if you define the language to the structs that are in the inputs to whatever is formally verified I guess whatever C like dialect of a language it implements must be.

I'm sure the programmers of the flight control software safely transporting 1 billion people per year see your "real world project" and reply with something like "yes, if you are writing software where the outputs don't matter very much, our processes are excessive" :p

It is only real-world project when it is about serializing and de-serializing JSON payloads.

Reply on news.ycombinator.com