an hour ago
I highly recommend checking out the other projects from AeneasVerif (and Jonathan Protzenko).
Scylla is kind of Eurydice's dual. But also Charon and the eponymous Aeneas.
Also, "There is ongoing work to integrate Eurydice-generated code for both Microsoft and Google’s respective crypto libraries." [1] which I find incredibly cool. This link is also a brilliant intro to Eurydice.
an hour ago
> readable C > return uu____0;
If readability is the selling point, why not go the extra millimeter and add a heuristic so that this variable is named return_value for instance?
7 hours ago
If it's readable C, this sounds great for a full source bootstrap of the rust compiler.
5 hours ago
Why would it need to be readable to be applicable to bootstrapping?
4 hours ago
It depends entirely on your trust model. If you just want to be able to compile a rust compiler on a new platform that only has a C compiler, you wouldn't care. If you worry about a Thompson-style trojan horse, then you want to be able to audit all sources in the bootstrap chain.
Some idealistic projects like live-bootstrap go a step further and don't even allow generated sources in the full source bootstrap chain, even if they are readable in principle, because the xz debacle showed that a configure script, which is also readable in principle, can contain a backdoor. In those projects you could probably still bootstrap Eurydice from sources, and then do the rust -> c translation of the rust compiler as an ordinary build step, before compiling it with a bootstrapped C compiler.
2 hours ago
> If you worry about a Thompson-style trojan horse, then you want to be able to audit all sources in the bootstrap chain.
Wouldn't you want to audit the final outputs? Except nobody is going to bother analyzing my hand all the assembly produced by the final tool.
In other words, I am not seeing the value of pursuing the discovery of Thompson-style Trojans, no matter what the original source language was. It is one of these risks that one has to live with.
2 hours ago
[dead]
13 hours ago
I wish this covered more features specific to rust that make it more runtime safer not just compile time safer. I guess by the time it's IR it's the same but moving it back up to C would be nice to see. Like bounds checking.
12 hours ago
I think those are covered. Any checks that Rust adds will be present in the IR (either coded in the original source or implied through rust semantics). Those checks would then get put in the compiled C output. The ideal output of Eurydice would be to have exactly the same semantics and safety as provided by Rust. Since their use case is to use Rust to code on platform without support for a rust compiler, it is a rather important goal to have too.
2 hours ago
Sorry not the software, I meant the article/write-up. I'm sure the software covers everything
8 hours ago
What an excellent choice of product name :D
"You're da C"
8 hours ago
"you read da c"
Only know the pronunciation due to hadestown
7 hours ago
Really more like "you're rid o(f) c" though, have you considered making it compile the other way
7 hours ago
Sorry but even threads about fringe mathematics are somewhat easier to decipher for me than this thread.
ELI5, anyone?
6 hours ago
"Eurydice" is pronounced roughly like each of the ancestor posts. (It isn't "you-ree-dice".)
an hour ago
Isn't "Eurydice" Greek, so I would expect it to be pronounced more like [eu̯.ry.dí.kɛː], so nothing remotely similar to "you"?
3 hours ago
> It isn't "you-ree-dice"
True, it is "you-ri-di-cee"
8 hours ago
D and C++ would benefit from something like this.
6 hours ago
Why?
C++ started as a preprocessor that translated into C, nowadays all relevant C compilers are written in C++.
D has enough backeds already available.
5 hours ago
People still maintain old versions of GCC just to maintain a bootstrap path.
I also think it would be helpful to how have a useful intermediate result to look at. So I agree, having C++ to C compiler would be useful.
3 hours ago
I don't see what's wrong with e.g. LLVM IR for that purpose.
C seems to me a really poor choice because it's barely more expressive than one of the machine code architectures and yet unlike them it's not even a real machine we can know about - some of the edge cases are just a shrug emoji.
The LLVM IR is buggy of course, and under-specified, but we could imagine improving those things more easily than fixing C for this purpose.
2 hours ago
In fact, looking at several languages since Fortran, some kind of minimal bytecode was a common approach.
That is also how Pascal P-Code started, UCSD reused and extend it for UCSD Pascal, however Niklaus Wirth designed it originally to port Pascal compilers.
Then he did it again with Modula-2 (M-Code), and Oberon (slim binaries, although here the idea came from Michael Franz).
Naturally there were many others, and best of all no UB surprises with backend optimisations.
an hour ago
Nothing against byte code for implementation, but it is also not readable.
It is easy to avoid UB surprises in C when generating code, so I do not think there is any good argument against C at this point.
3 hours ago
C is a lot more readable than assembly or LLVM IR, so no - do not agree it that is a poor choice. I also do not see the edge cases in practice.
33 minutes ago
Both you and I think C is more readable than LLVM IR but I'm not at all convinced that's just universally true -- I think it's because we're both experienced C programmers and so it's just our bias.
In particular I think LLVM's poison and undef values are valuable for understanding what some C++ means and why. Seeing that some C++ ends up as a select to choose between certain values, some of which are poison, makes it apparent why an optimisation choice is sound or not, where the likely C would leave this unsaid.
5 hours ago
Intermediate result is the compilation to Assembly source code, and C++ insights like tooling.
Those people should move on, there isn't a single relevant platform without at least C++98 compiler, and there are other ways to bootstrap compilers.
4 hours ago
For platforms not having a D compiler.
The C++ subset target is of theoretical interest and because some compilers cannot support a C++ compiler of the latest standard. OpenWatcom comes to mind.
Of course the question is which C++ standard in and what C standard out!
3 hours ago
So target C++98, or C++ARM.
As for not having a compiler, do it like in the old days, cross compilation.
See Go and Zig for good examples of old practices brought into modern times.
2 hours ago
Apprently https://edgcpp.org/ can do that for C++. I dunno why you'd need to though?
7 hours ago
the circle is complete
an hour ago
I wonder if you keep compiling back and forth would you ever hit a cycle or would it be constantly growing?
12 hours ago
[flagged]
10 hours ago
[flagged]