writing proofs in lean feels just like coding except your entire program is a noop and your only job is to make it typecheck - ThreadSky

danabra.mov • 10 days ago

writing proofs in lean feels just like coding except your entire program is a noop and your only job is to make it typecheck

Comments

brandonherrell.bsky.social•9 days ago

No disrespect but even knowing these words is thought cancer

jds-bv.bsky.social•10 days ago

@danabra.mov What was your motivation to look into lean, "just" intellectual curiosity or do you have some application in mind if I may ask?

danabra.mov•10 days ago

i like pure math because it’s useless! (sort of.)

jds-bv.bsky.social•10 days ago

I studied mathematics, so I see it too as a beautiful topic and I like both the playful aspects as well as the timelessness and authority of mathematical truth which by itself is "enough". But since I am mostly a programmer these days, I am always on the lookout for practical application, too. 😉

raging-uke-kazu.bsky.social•10 days ago

HEY. I literally don't know how to advertise a fundraiser so all I'm able to do is post the link wherever I can to get as may eyes on it as possible. We're desperate. We literally just want to live a quiet peaceful life as a family somewhere safe.
https://gofund.me/dc81cd08

fundmystartup.bsky.social•9 days ago

Ok, so lean is a proof assistant and functional programming language.

bobappleyard.bsky.social•9 days ago

curry howard isomorphism innit

e1k1.bsky.social•3 days ago

Not a no-op at all! If you were ever to run it, it would take proofs of hypotheses and emit a proof of the conclusion.

staja84f.bsky.social•10 days ago

So the quote for
Woody Allen on casual sex would apply here: “it’s an empty and meaningless experience, but as far those go, it’s pretty good”

bronzegoddess1.bsky.social•9 days ago

I hate coding. It seems so hard 😭

rhino0131.bsky.social•9 days ago

I have no idea what you're talking about or why it's on my time line, but sounds good! 👍

paxdriver.bsky.social•10 days ago

So it's like writing javascript using only prototypes instead of instructions? Lol that's sounds like a wickedly fun challenge!

dialupready.com•10 days ago

same with Coq, and the VSCode extension is quite good at pointing errors and reverifying immediately

proof assistants are so cool, working through Software Foundations (https://softwarefoundations.cis.upenn.edu/) was fun even if it was an assignment

brundolf.bsky.social•10 days ago

guys only want one thing and it's disgusting

paxdriver.bsky.social•10 days ago

Javascript? Lol 😜

Comments

Posting Rules

Reply