Alex

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.