Personally I really don’t like it too. But I just don’t care because:

• I have all needed software locally
• I have all documentation locally
• I’m going to Web only to get updates (by-hands of course, no autoupdates without verification!)
• I’m old software engineer and how to automate it all without losing ctrl ;)

Oh, how long we’ve been waiting for this! ❤️‍🔥🎉 Great paper, but why default coq was chosen? That’s totally okay (and coq is still kinda default for interactive formal proving), but there is others production-ready strong modern instruments existing on Earth today. Just interesting why so.

For me personally, the “retro” is about period ending before “age of ugliest 3D”.

f16 and f128

Great!👍🏻 What about FPU and VFP support?

Done!

Ok, understood, thank you.

I’m not sure is it sarcasm or that’s really not bad short description? 🤔

Trying to reduce compilation time, reconfiguring underlying cargo’ build-ctx or just riding off the context and using only build-plan and metadata by host cargo & rustc in the cargo-playdate tool.

Nope. This little neat feature mainly is just necessary part of bigger one - const-generics with const bounds.

Did author knows about difference between static and dynamic dispatch? 🤦🏻‍♂️

Okay, just take a look at code. https://github.com/aeharding/voyager

Just one question - where it is native? Are you pretty sure?