if i had to describe Lean in a few sentences, i’d say that in Lean, each statement you’d think of as boolean (e.g. “is X equal to Y?”) is itself a type. so you can construct proofs, which are objects *of* that type. so a function can accept a number X *and also* a proof of “X is even” or “X > 10”

does flashes need app password or something? i was hoping for oauth

i sort of like this. i was also considering this angle. i’m only worried that my previous introductions to dependent types were quite inaccessible and i sort of assumed they’re a more academic concept. whereas with Lean i just directly encountered their awesomeness RE:

Bluesky Social

Rado Kirov (@radokirov.bsky.social)

I have been thinking about this too, and here is my proto-pitch - "Dependent Types with Lean for the curious TypeScript developers". Not sure how m...

yea i was just thinking yesterday atproto will probably eventually win but it may take twenty years RE:

Bluesky Social

Laurens (@laurenshof.online)

also whats interesting about open internet protocols is that its quite obvious that this shift is going to happen at some point, but pretty much ev...

if you want to send me seething with primal rage, use the verb “claim” somewhere in your app copy as a call to action, like “claim your free…” ahhh fuck you fuck you fuck you fuck you

i’m “considering” (aka: never gonna happen) writing an introduction to Lean for JavaScript developers. if that’s you, what do you want to know? do you have any specific questions

it’s happening 👀 [github.com/facebook/rea...](

GitHub

[Fiber] Deprecate "Throw a Promise" technique by sebmarkbage · Pull Request #34032 · facebook/react

This has been replaced by React.use(promise) which in turn should be used unconditionally if data is depended upon. The "throw a Promise"...

) [[Fiber] Deprecate "Throw a Pro...](

GitHub

[Fiber] Deprecate "Throw a Promise" technique by sebmarkbage · Pull Request #34032 · facebook/react

This has been replaced by React.use(promise) which in turn should be used unconditionally if data is depended upon. The "throw a Promise"...

)

sketched an intuition for how a Lean proof maps to a proof of the same statement written in the traditional mathematical style https://morel.us-east.host.bsky.network/xrpc/com.atproto.sync.getBlob?did=did:plc:fpruhuo22xkm5o7ttr2ktxdo&cid=bafkreibaendvpcfp6u2mrhvufch25gxn5lm3cky4ztjz3e72mi3zalywy4

today i spent all day on this exercise. after a lot of back and forth with Claude i figured it out, but it was hard. the goal is to construct a set of all partial functions (all functions from subsets of X to subsets of Y). the mindfuck was that i can "manifest" X' and Y' i don’t know by using ∃ https://morel.us-east.host.bsky.network/xrpc/com.atproto.sync.getBlob?did=did:plc:fpruhuo22xkm5o7ttr2ktxdo&cid=bafkreifypuxaaz3r7ud4ewz6zndrntr4lqdhjggdc4ss46klj5clvmpb2y

claude when it poisons the context RE:

Bluesky Social

Bluesky