Conversation

Notices

1. Embed this notice
   julesh (julesh@mathstodon.xyz)'s status on Wednesday, 18-Dec-2024 02:34:29 JST julesh

   Prediction: over the next decade or 2 the remaining basic principles of proof assistants will be figured out, and the first minimally viable language will be proudly handed over to the mathematicians, who will then look at the millions of lines of code they've already written in Lean and collectively decide to just keep building on that. Only another decade or 2 after that will they learn the meaning of "technical debt"

   • Embed this notice
     John Carlos Baez (johncarlosbaez@mathstodon.xyz)'s status on Wednesday, 18-Dec-2024 02:53:57 JST John Carlos Baez

     in reply to

     @julesh - in a sense ZFC set theory is a massive mountain of technical debt. Most mathematicians just keep building on it.

   • Embed this notice
     Σ(i³) = (Σi)² (svengeier@mathstodon.xyz)'s status on Wednesday, 18-Dec-2024 16:53:49 JST Σ(i³) = (Σi)²

     in reply to

     @julesh
     Real programmers can write FORTRAN programs in any language!

   • Embed this notice
     julesh (julesh@mathstodon.xyz)'s status on Wednesday, 18-Dec-2024 19:49:19 JST julesh

     in reply to

     • NoCanDo

     @escape_velocity Personally I think interacting with a programming language through a text editor buffer is extremely backward, it's a historical leftover from the 20th century that for some reason we haven't got rid of yet. You want at least some kind of interactive, syntax-aware editing and trying to do that with a text editor is putting a square peg in a round hole. Even a web browser interface would be an improvement

   • Embed this notice
     NoCanDo (escape_velocity@functional.cafe)'s status on Wednesday, 18-Dec-2024 19:49:20 JST NoCanDo

     in reply to

     @julesh I sincerely doubt that. For one, lean might have a ZFC model, but it is still a CoC system + UIP + 3 axioms. Secondly, mathematicians don't give two hoots about ZFC or any foundations. I learnt this only 2-3 years ago. Talking about foundations is pretty much the same as flogging a dead horse that can never be revived by any magic. With mathlib and lean, this conversation has become even more difficult. Thirdly, in lean, especially mathlib, definitions are separated from useful theorems by a layer of API lemma. So if definitions have to change while maintaining the same properties, only the API lemmas need to be reproved. Everything else stays the same, unless something fundamentally changes in the type system.

     Finally IMHO, among other socio-cultural things, what made lean so popular today is UX. When this perfect proof system is built, I hope the developers invest heavily in UX. Someone might build the greatest proof system on the planet, but if they insist on pushing UX of a bygone era, then the system will never compete against another with better UX. Tooling matters. Easy package management matters*. In general, the "boring" stuff matters. Much more than interesting foundational conundrums or features. If a language does not have decent editor support (that means vscode today), then I am not touching it with a barge pole. I still poke around in other ITPs and even enjoy them a bit, but none can yet match lean's editor support. That's the biggest lesson I learnt from the lean community.

     * lean's highly annoying and deficient package management still feels leaps and bounds ahead of what I have seen in other ITPs