Yeah, but they now seem totally uninterested in converging. I'm happy to translate some of the ideas over to cubical, I'm generally good at that kind of thing, but it helps to have experts on both sides of the bridge interested
Conversation
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Fair, I just think for your every day humans, automation and usability are what will matter. Another thing I'm happy to help with is building search procedures that discover and prove type equivalences automatically
3
3
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
From a talk I saw (recorded from a Lean users conference thing they had at the beginning of the year) they seemed like they were open to improvements, but wanted really clear, concrete proposals, ideally with realistic plans to implement.
2
3
This is the bit I was referring to, fwiw (time stamp 1:06:51):
2
3
On the slide before that they went into what their next steps were, and it sounded like they had a huge amount on their plate, and not a lot of time to spend on communication.
1
1
All of us have huge amounts of things on our plates, that isn't a good reason to alienate people who are interested in our work
1
2
Yeah - as somebody who helped out with Rust in the early days, I much prefer that approach to development. It definitely has lots of challenges but I think its worth it in the long run to make communities more open and less alienating.