L
@llllvvuu.dev
Reposted by L
This StackOverflow answer about referential transparency by Uday Reddy is absolutely wonderful stackoverflow.com/questions/21...
April 23, 2024 at 3:50 PM
This StackOverflow answer about referential transparency by Uday Reddy is absolutely wonderful stackoverflow.com/questions/21...
I still think it's hilarious that Facebook made "updating relationship status" a feature, and as if that wasn't enough, added "it's complicated" as an option. The mind of Zuck lmao
April 5, 2024 at 6:40 PM
I still think it's hilarious that Facebook made "updating relationship status" a feature, and as if that wasn't enough, added "it's complicated" as an option. The mind of Zuck lmao
every few years i remember rock music is actually pretty good
April 4, 2024 at 9:09 AM
every few years i remember rock music is actually pretty good
This app has gotten a lot better since I last checked. Used to be a lot of missing UI polish, slow perf, state management issues
April 3, 2024 at 3:44 AM
This app has gotten a lot better since I last checked. Used to be a lot of missing UI polish, slow perf, state management issues
The predictability of GOFAI is really handy in "prompt engineering" in Lean 4. i.e. nudging (`have`, `suffices`, `calc`, `rw`, `refine`) the goal(s) into state(s) that can be killed by tactics (`simp`, `fun_prop`, `ring`). This golfing art is more reliable and satisfying than prompting Copilot.
February 16, 2024 at 11:34 AM
The predictability of GOFAI is really handy in "prompt engineering" in Lean 4. i.e. nudging (`have`, `suffices`, `calc`, `rw`, `refine`) the goal(s) into state(s) that can be killed by tactics (`simp`, `fun_prop`, `ring`). This golfing art is more reliable and satisfying than prompting Copilot.
Maybe because I've been a programmer and not a math student for too long, but:
Sometimes I actually prefer to read Lean than mathematical English. It is 20x as lengthy but 100x (source: I made it up) more explorable.
Sometimes I actually prefer to read Lean than mathematical English. It is 20x as lengthy but 100x (source: I made it up) more explorable.
January 11, 2024 at 12:43 AM
Maybe because I've been a programmer and not a math student for too long, but:
Sometimes I actually prefer to read Lean than mathematical English. It is 20x as lengthy but 100x (source: I made it up) more explorable.
Sometimes I actually prefer to read Lean than mathematical English. It is 20x as lengthy but 100x (source: I made it up) more explorable.
This was a trippy little lemma for Lean:
In plain math, one wouldn't even bother to go into detail on the highlighted line, since it's obvious.
But there are actually multiple ways to arrive at it, which makes all the difference for coding it in Lean!
leanprover.zulipchat.com#narrow/strea...
In plain math, one wouldn't even bother to go into detail on the highlighted line, since it's obvious.
But there are actually multiple ways to arrive at it, which makes all the difference for coding it in Lean!
leanprover.zulipchat.com#narrow/strea...
January 10, 2024 at 9:33 PM
This was a trippy little lemma for Lean:
In plain math, one wouldn't even bother to go into detail on the highlighted line, since it's obvious.
But there are actually multiple ways to arrive at it, which makes all the difference for coding it in Lean!
leanprover.zulipchat.com#narrow/strea...
In plain math, one wouldn't even bother to go into detail on the highlighted line, since it's obvious.
But there are actually multiple ways to arrive at it, which makes all the difference for coding it in Lean!
leanprover.zulipchat.com#narrow/strea...
Lean is really like New Game+ for math. Just getting mauled by the most trivial stuff
the one property it shares in common with non-computerized math is that whenever you look at what you wrote, you feel stupid for how long it took
the one property it shares in common with non-computerized math is that whenever you look at what you wrote, you feel stupid for how long it took
December 7, 2023 at 5:03 AM
Lean is really like New Game+ for math. Just getting mauled by the most trivial stuff
the one property it shares in common with non-computerized math is that whenever you look at what you wrote, you feel stupid for how long it took
the one property it shares in common with non-computerized math is that whenever you look at what you wrote, you feel stupid for how long it took
food: $500
rent: $1000
charges from aws that don't show up on any of like 10 accounts: $1000000
please help me budget this my family is dying
rent: $1000
charges from aws that don't show up on any of like 10 accounts: $1000000
please help me budget this my family is dying
December 1, 2023 at 11:51 PM
food: $500
rent: $1000
charges from aws that don't show up on any of like 10 accounts: $1000000
please help me budget this my family is dying
rent: $1000
charges from aws that don't show up on any of like 10 accounts: $1000000
please help me budget this my family is dying
If we are to believe:
- openai's "scaling laws"(data must grow at compute^0.27)
- moore's law
- baumol's cost disease
won't AI eventually be bottlenecked on the phillipines?
- openai's "scaling laws"(data must grow at compute^0.27)
- moore's law
- baumol's cost disease
won't AI eventually be bottlenecked on the phillipines?
November 30, 2023 at 7:23 AM
If we are to believe:
- openai's "scaling laws"(data must grow at compute^0.27)
- moore's law
- baumol's cost disease
won't AI eventually be bottlenecked on the phillipines?
- openai's "scaling laws"(data must grow at compute^0.27)
- moore's law
- baumol's cost disease
won't AI eventually be bottlenecked on the phillipines?
if you like refactoring or golfing you'll love Lean
November 28, 2023 at 8:24 AM
if you like refactoring or golfing you'll love Lean
November 17, 2023 at 1:41 AM
Seems like a lot of developers have reproducibility issues with Foundry, so I made an asdf plugin (s/asdf/rtx):
github.com/llllvvuu/asd...
(it's a bit janky rn since not every release has all the tarballs)
github.com/llllvvuu/asd...
(it's a bit janky rn since not every release has all the tarballs)
November 6, 2023 at 1:04 PM
Seems like a lot of developers have reproducibility issues with Foundry, so I made an asdf plugin (s/asdf/rtx):
github.com/llllvvuu/asd...
(it's a bit janky rn since not every release has all the tarballs)
github.com/llllvvuu/asd...
(it's a bit janky rn since not every release has all the tarballs)
Reposted by L
The cum feed is back!
October 23, 2023 at 6:31 PM
The cum feed is back!
Reposted by L
The cum feed is broken :(
October 22, 2023 at 11:45 PM
The cum feed is broken :(
Is it just me or was typography really good back in the days? Like random food packaging and appliances look way better than any website
October 19, 2023 at 9:18 PM
Is it just me or was typography really good back in the days? Like random food packaging and appliances look way better than any website
Something I wonder with products like @cursor_ai: whether "context engineering" will go away like "prompt engineering" is kinda going away
i.e. eventually you may always want to "search entire codebase" or even "search entire world" instead of manually attaching specific files
i.e. eventually you may always want to "search entire codebase" or even "search entire world" instead of manually attaching specific files
October 13, 2023 at 1:23 PM
Something I wonder with products like @cursor_ai: whether "context engineering" will go away like "prompt engineering" is kinda going away
i.e. eventually you may always want to "search entire codebase" or even "search entire world" instead of manually attaching specific files
i.e. eventually you may always want to "search entire codebase" or even "search entire world" instead of manually attaching specific files
Pretty interesting nerd snipe... who knew that proof x = step proof half x, is so hard to check
(I actually have no idea how I'd write such a checker)
podcasts.google.com/feed/aHR0cHM...
(I actually have no idea how I'd write such a checker)
podcasts.google.com/feed/aHR0cHM...
September 21, 2023 at 8:07 PM
Pretty interesting nerd snipe... who knew that proof x = step proof half x, is so hard to check
(I actually have no idea how I'd write such a checker)
podcasts.google.com/feed/aHR0cHM...
(I actually have no idea how I'd write such a checker)
podcasts.google.com/feed/aHR0cHM...
September 19, 2023 at 6:15 PM
initial thoughts on structural/"projectional" editing - is it necessary for users to buy into a whole new language, toolchain, ecosystem, *and* editor? and to require the resources to actually build all these?
1/5
1/5
September 19, 2023 at 3:36 AM
initial thoughts on structural/"projectional" editing - is it necessary for users to buy into a whole new language, toolchain, ecosystem, *and* editor? and to require the resources to actually build all these?
1/5
1/5
Idea for an AI tool - commit unsquasher. e.g. when you see a thousands of line commit that does multiple things that you need to find a regression in. Or you just want to reorganize a commit log.
September 15, 2023 at 5:12 AM
Idea for an AI tool - commit unsquasher. e.g. when you see a thousands of line commit that does multiple things that you need to find a regression in. Or you just want to reorganize a commit log.
my thinking on no-code: once there are enough tools/widgets to need a search bar, it's coding
an IDE is just an omnibar for browsing and trying out widgets
i'm not an expert but this what literally what "coding" means in the medical field isn't it?
an IDE is just an omnibar for browsing and trying out widgets
i'm not an expert but this what literally what "coding" means in the medical field isn't it?
September 11, 2023 at 9:57 PM
my thinking on no-code: once there are enough tools/widgets to need a search bar, it's coding
an IDE is just an omnibar for browsing and trying out widgets
i'm not an expert but this what literally what "coding" means in the medical field isn't it?
an IDE is just an omnibar for browsing and trying out widgets
i'm not an expert but this what literally what "coding" means in the medical field isn't it?