• Alex@programming.dev
    link
    fedilink
    arrow-up
    2
    ·
    edit-2
    2 days ago

    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.