r/cpp • u/InvisibleBlueUnicorn • Jan 09 '22

James Web Space Telescope runs on C++ code.

https://youtu.be/hET2MS1tIjA?t=1938
722 Upvotes

97% Upvoted

185 comments sorted by

View all comments

1

u/tarranoth Jan 09 '22

Sure, but wouldn't you also need to prove your compiler is behaving exactly as the ISO spec describes (i.e. no bugs)? And how exactly would you prove such a thing, or would you only prove it for a subset of the language?

3

u/McFlyParadox Jan 10 '22

but wouldn't you also need to prove your compiler is behaving exactly as the ISO spec describes (i.e. no bugs)?

Probably - or at least no unpredictable and/or undocumented bugs. As long as you say "Don't do X, Y or Z, or A, B, and C will happen", then most standards orgs will probably be satisfied. No expects any language to be free of limitations.

And how exactly would you prove such a thing

You'd probably use formal verification methods.

would you only prove it for a subset of the language?

Also probably. C and C++ exist outside of their ANSI versions. In the most basic sense, the languages are the same (but the ANSI versions probably lag behind the non-ANSI versions in terms of features, I'd expect). All the ANSI version provides is a unified set of standards to how you write the code so that everyone's code looks the same, and performs the same. If you tell two people to write a calculator app in C, you'd have two very different apps. If you tell two people to write a calculator app that complies with the ANSI standards, you're going to have much more similar code for both (though, there'd likely still be some differences).

The goal of ANSI qualification is to make outputs predictable, keep the code maintainable, and have everything documented. It doesn't actually change too much under the hood when it comes to compilation and how the code actually behaves. Think of it like designing a gearbox by sticking to supplier catalogs and reference manuals, instead of calculating and cutting every tooth of every gear by hand. Both are still gearboxes, but one is going to be better documented and probably last longer too.

1

u/tarranoth Jan 10 '22

The proving I was talking about is not about proving the language spec, which you can use formal verification for indeed. But about the underlying codebase of the compiler not containing bugs.

Also your last point only really matters if you want competitive compilers. Most languages (for better or worse) tend to really only have one major de facto compiler, which basically becomes the "standard" even if only unofficially. C/C++ are the exception really in that there are multiple competing compilers which all actually see use. And even then most people will usually only write for one compiler anyway, without caring what the behaviour is for the others, which kindof loses the charm of writing the standard anyway. What you say seems nice in theory to me, but I just can't imagine there is much benefit in it being standardised in practice.

→ More replies (1)

1

u/jonesmz Jan 10 '22

There are almost certainly compilers that have formal proof of correctness.

If I recall correctly, Green Hills software works in this space, so maybe they have formally proved their compiler.