27

Proposal: Proof Assistants

EDIT: Due to a backlog of stuff accumulated over the Winter 2021 holidays, this site's launch was moved to February 2022. More info here.

Since we want all proposals to have the best chances of thriving as possible, the Community Team has decided to postpone this proposal's launch into private beta to January 2022, in an attempt to minimize the impact of the upcoming end-of-year holidays in the site's chances of success.

Additionally, the proposal sped through its definition and commitment phases, which we believe hasn't allowed for some discussions that usually take place during those phases — such as deciding on a name and URL for the site — to come to a consensus. As such, we invite those of you who've committed to this proposal to try to have those conversations between now and the first couple of weeks of January 2022. At that time the Community Team will help y'all tie whatever loose ends need to be tied, and prepare the site for launch into private beta.

19
  • The problem with this is that many people may not care any more if this ever starts. At this point I am quite happy on the Zulip sites.
    – Guy Coder
    Commented Dec 9, 2021 at 13:37
  • 8
    I understand that momentum is important in this process, @GuyCoder, but your suggestion that postponing the launch for a month may mean no one will be interested in the site at that point worries me.
    – JNat StaffMod
    Commented Dec 9, 2021 at 15:20
  • @JNat I can only speak for myself but as I noted early on I set a checkpoint of 6 months to decide if this site is adding value to the communities using proof assistants. This notice shows me that one of those months are now gone. Also by delaying till January many of those teaching university courses who may direct students to this may be hesitant do so because they will not know exactly when the site is up. Currently they have established means for Q&A, so by delaying it may not be until the fall of 2022 that a push is seen of new users. Just my humble opinion.
    – Guy Coder
    Commented Dec 9, 2021 at 15:37
  • @JNat Here are the places I relayed this notice. Zulip Lean, Zulip Coq, Zulip Isabelle, continued.
    – Guy Coder
    Commented Dec 9, 2021 at 15:43
  • 1
    Personally, I feel like the momentum has already been lost with the delay since 100% commitment, so a few more weeks is neither here nor there. From now on, we should see a realistic level of activity.
    – mudri
    Commented Dec 10, 2021 at 9:42
  • 14
    Although I am disappointed by delay, I am confused and confounded by these claims from mudri and Guy Coder that momentum will have disappeared by then. It's not like my questions will have "dried up" in a month's time...
    – Alex Nelson
    Commented Dec 10, 2021 at 15:49
  • 2
    Is it possible to update the header on the proposal to indicate that "this launch is on hold until January 2022" so those browsing to it will easily know? This was done with the various "SO in [language]" proposals before they were closed and deleted.
    – damryfbfnetsi
    Commented Dec 11, 2021 at 21:55
  • 1
    Done, @damryfbfnetsi ;)
    – JNat StaffMod
    Commented Dec 13, 2021 at 15:03
  • 12
    No worries, I am sure we can build the momentum again. The real test is what happens in the long run.
    – Andrej Bauer
    Commented Dec 16, 2021 at 10:35
  • 3
    @JNat Any updates about the projected start date?
    – Alex Nelson
    Commented Jan 9, 2022 at 18:49
  • 2
    Apologies for the delay in responding, @AlexNelson — we're still catching up from a bit of a backlog that accumulated over the holidays, and will update y'all once we have news.
    – JNat StaffMod
    Commented Jan 12, 2022 at 16:50
  • 1
    @JNat No worries about the belated response! The holidays are always a busy time, I understand, and I appreciate your time and attention :)
    – Alex Nelson
    Commented Jan 12, 2022 at 17:47
  • 6
    Juggling a few things at the moment, but hope to have an update for you by the end of the week.
    – JNat StaffMod
    Commented Jan 18, 2022 at 18:29
  • 7
    It is currently scheduled to take place in the first week of February, @HenryWHHackv3.0b
    – JNat StaffMod
    Commented Jan 19, 2022 at 13:38
  • 2
    @JNat Can you please edit this announcement and the banner on the proposal to reflect this? Also, what about the Substrate proposal: can you please answer its question asking when it'll be launched?
    – damryfbfnetsi
    Commented Jan 20, 2022 at 20:03

1 Answer 1

Reset to default
8

Are there things we can help with at present, or is there nothing for us to do but celebrate the holidays?

P.S. It's super cool that if I start my answer with "Dear SE overlords," that bit just gets erased. I am now tempted to try "Long live SE overlords" as my closing.

1
  • 5
    It's the "Dear X" that gets removed by default from the SE software, IIRC. Likewise ending questions with things like "Thanks"
    – David Roberts
    Commented Dec 27, 2021 at 3:28

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .