Huh, I read the pitch differently. As "reduce risk of (failure through artificial intelligence)," not as "(reduce risk of failure) through artificial intelligence." Maybe that's my bias since that's what I'm working on,…
Not the author, but I've been doing this kind of thing with Lean. I'm still trying to figure out how to make this workflow play nicely with other systems. I have a bunch of rust code that I want these kinds of…
I've been experimenting with this a lot lately in Lean because it's equally capable as a theorem prover and as a programming language. It's resolving a lot of the frustration I feel with LLM coding. You write a type…
I remember trying to play around with Coq/Rocq and a few others about 15 years ago, and I couldn’t make heads or tails of them. Not the concepts, but the software. What’s weird about proof assistants/interactive provers…
Complex numbers and Schwartz distributions (the thing the dirac delta is) come immediately to mind. “Not all numbers have square roots, but what if they did?” It seems like a common pattern.
That works until you make a plan/tests/etc, set the thing loose, and then when it has trouble it decides "actually the pragmatic thing would be [diverge from the plan/change the tests/etc]" and goes off the rails. I'm…
I like the Kronecker quote, "Natural numbers were created by god, everything else is the work of men" (translated). I figure that (like programming) it turns out that putting our problems and solutions into precise…
I always mentally slotted prosemirror-collab/your recommended solution in the OT category. What’s the difference between the “rebase” step and the “transformation” step you’re saying it doesn’t need?
Two things come to mind: - Whatever you measure gets optimized. - When a measure becomes a target, it ceases to be a good measure. I have no idea which is more relevant here. Looking at the first one, my whole life…
On the topic, do you know any approaches to infitesimals/differentials that do cotangents and pullbacks as primitives? In practice, I always end up needing to work in cotangents, but deriving them is always roundabout…
Any chance you know of good DAE books/resources that go into combining symbolics and numerics or parametrized DAEs?
This is a thing I'm working on, so I have some potentially useful thoughts. tl;dr, it doesn't have to be about encoding arbitrary real life statements to be super duper useful today. > how might an arbitrary statement…
Location: San Francisco, California Remote: Ideally hybrid Willing to relocate: No Technologies: Pytorch, JAX, spark, and the rest of the python data ecosystem; AWS; Python, C, R, SQL, Java Resume/CV: CV link…
I’d expand “tech” beyond computers. I’ve recently gotten into mini painting and sculpting. I can get paints and brushes and magic epoxy putties and sculptable thermoplastics and precision tools for less than a nice…
Excel is kind of WYSIWYG programming. I use it for quick stuff frequently and I’m amazed at what it makes easier than e.g. numpy. There’s a whole class of error you don’t make because you see the whole intermediate…
Remember that unlicensed content is still licensed. Generally the implicit license of a work is less permissive. So however you feel about this using GPL code, the situation is even worse for most ML models that have no…
Unlicensed code just means “all rights reserved.” You’d need to limit it to permissively licensed code and make sure you comply with their requirements.
What a fantastic post. > Is ‘folk wisdom from internet forums’ worth exploring as a genre of blog post? I’d add another yes here, if they’re all as thorough as this post. I’ll add something that I didn’t see directly…
We used to not understand how steam engines worked either, even once we got them working. At least not past the most macro level. Understanding at the micro level came later.
Rather than being a suppressed topic, in my experience, this is a case of people talking past each other. It's like correlation versus causation (versus plain old connected definitions). It can be true that A and B are…
It wouldn't be a smooth app, but it would still render, which would be fun to play with.
Hi! Thanks for engaging with the comments. I believe you've misunderstood the main point of my comment. I don't have too strong opinions about reshape vs newaxis. The real point was about excessive inlining, which your…
> I'd prefer if the language only had a single number type (maybe configurable at once by an external option) and a single sqrt function. If you meant a numeric single type class, like haskell's Num, I think it's a…
I got bored with trying to find an analytical boost, but I benchmarked a couple IMO super readable python versions (basically what's in my original comment after making the (100+i)i change):…
Regarding your performance work, you've nerd sniped me into looking for analytical tricks to speed it up ;) We'll see... Regarding the readability, I suppose it's a matter of taste at this point, but if I swapped…
Huh, I read the pitch differently. As "reduce risk of (failure through artificial intelligence)," not as "(reduce risk of failure) through artificial intelligence." Maybe that's my bias since that's what I'm working on,…
Not the author, but I've been doing this kind of thing with Lean. I'm still trying to figure out how to make this workflow play nicely with other systems. I have a bunch of rust code that I want these kinds of…
I've been experimenting with this a lot lately in Lean because it's equally capable as a theorem prover and as a programming language. It's resolving a lot of the frustration I feel with LLM coding. You write a type…
I remember trying to play around with Coq/Rocq and a few others about 15 years ago, and I couldn’t make heads or tails of them. Not the concepts, but the software. What’s weird about proof assistants/interactive provers…
Complex numbers and Schwartz distributions (the thing the dirac delta is) come immediately to mind. “Not all numbers have square roots, but what if they did?” It seems like a common pattern.
That works until you make a plan/tests/etc, set the thing loose, and then when it has trouble it decides "actually the pragmatic thing would be [diverge from the plan/change the tests/etc]" and goes off the rails. I'm…
I like the Kronecker quote, "Natural numbers were created by god, everything else is the work of men" (translated). I figure that (like programming) it turns out that putting our problems and solutions into precise…
I always mentally slotted prosemirror-collab/your recommended solution in the OT category. What’s the difference between the “rebase” step and the “transformation” step you’re saying it doesn’t need?
Two things come to mind: - Whatever you measure gets optimized. - When a measure becomes a target, it ceases to be a good measure. I have no idea which is more relevant here. Looking at the first one, my whole life…
On the topic, do you know any approaches to infitesimals/differentials that do cotangents and pullbacks as primitives? In practice, I always end up needing to work in cotangents, but deriving them is always roundabout…
Any chance you know of good DAE books/resources that go into combining symbolics and numerics or parametrized DAEs?
This is a thing I'm working on, so I have some potentially useful thoughts. tl;dr, it doesn't have to be about encoding arbitrary real life statements to be super duper useful today. > how might an arbitrary statement…
Location: San Francisco, California Remote: Ideally hybrid Willing to relocate: No Technologies: Pytorch, JAX, spark, and the rest of the python data ecosystem; AWS; Python, C, R, SQL, Java Resume/CV: CV link…
I’d expand “tech” beyond computers. I’ve recently gotten into mini painting and sculpting. I can get paints and brushes and magic epoxy putties and sculptable thermoplastics and precision tools for less than a nice…
Excel is kind of WYSIWYG programming. I use it for quick stuff frequently and I’m amazed at what it makes easier than e.g. numpy. There’s a whole class of error you don’t make because you see the whole intermediate…
Remember that unlicensed content is still licensed. Generally the implicit license of a work is less permissive. So however you feel about this using GPL code, the situation is even worse for most ML models that have no…
Unlicensed code just means “all rights reserved.” You’d need to limit it to permissively licensed code and make sure you comply with their requirements.
What a fantastic post. > Is ‘folk wisdom from internet forums’ worth exploring as a genre of blog post? I’d add another yes here, if they’re all as thorough as this post. I’ll add something that I didn’t see directly…
We used to not understand how steam engines worked either, even once we got them working. At least not past the most macro level. Understanding at the micro level came later.
Rather than being a suppressed topic, in my experience, this is a case of people talking past each other. It's like correlation versus causation (versus plain old connected definitions). It can be true that A and B are…
It wouldn't be a smooth app, but it would still render, which would be fun to play with.
Hi! Thanks for engaging with the comments. I believe you've misunderstood the main point of my comment. I don't have too strong opinions about reshape vs newaxis. The real point was about excessive inlining, which your…
> I'd prefer if the language only had a single number type (maybe configurable at once by an external option) and a single sqrt function. If you meant a numeric single type class, like haskell's Num, I think it's a…
I got bored with trying to find an analytical boost, but I benchmarked a couple IMO super readable python versions (basically what's in my original comment after making the (100+i)i change):…
Regarding your performance work, you've nerd sniped me into looking for analytical tricks to speed it up ;) We'll see... Regarding the readability, I suppose it's a matter of taste at this point, but if I swapped…