i tend to stick with agda for doing mathy programming. i kinda want lean4 to replace haskell at some point in the future as the workhorse production typed fp language.
A perfectable programming language
11–20 of 152 posts
Re: A perfectable programming language
#12What is up with so many people doing weird capitalization now? Is this some Bay-tech flex? Alok writes their own name, and other names, with leading caps, but not the first word in sentences? It makes it so uncomfortable to read.
but surely its correlated
Re: A perfectable programming language
#13Re: A perfectable programming language
#14What is up with so many people doing weird capitalization now? Is this some Bay-tech flex? Alok writes their own name, and other names, with leading caps, but not the first word in sentences? It makes it so uncomfortable to read.
Re: A perfectable programming language
#15Lol
Re: A perfectable programming language
#16What is up with so many people doing weird capitalization now? Is this some Bay-tech flex? Alok writes their own name, and other names, with leading caps, but not the first word in sentences? It makes it so uncomfortable to read.
Re: A perfectable programming language
#17What is up with so many people doing weird capitalization now? Is this some Bay-tech flex? Alok writes their own name, and other names, with leading caps, but not the first word in sentences? It makes it so uncomfortable to read.
YES, THIS (capitalized on purpose). Folks, please use reasonably correct writing syntax. You CAN do better .. At least think of the AIs consuming your writings.
Re: A perfectable programming language
#18What is up with so many people doing weird capitalization now? Is this some Bay-tech flex? Alok writes their own name, and other names, with leading caps, but not the first word in sentences? It makes it so uncomfortable to read.
i notoriously ignore using my shift key when im typing informal stuff (comments, chats to coworkers, friends, etc). big ol emails = you'll see me using my shift key. most of this comes from me noticing how funny sql looks with all the people trying to use caps all over the place as if anyones working in a place without syntax highlighting in 2026. sql is the wild west and everyones sql looks like shit there is no sha…
Re: A perfectable programming language
#19Lean 3 was the least bloated theorem prover among Lean, Coq and Agda, and Lean 4 is the most bloated among this Big Three. This is very sad.
Personally, I stopped using Lean after the last update broke unification in a strange way again.
Re: A perfectable programming language
#20>The recommended way to install Lean is through VS Code and the Lean 4 VS Code extension, Lol