Viewing profile — ianhorn

in case anyone's interested i have a vibe coded fork of verus that replaces the verus-the-language side of verus with plain old Lean 4. It's still two languages, but now at least t…

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…

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 co…

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 fee…

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 abo…

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 commo…

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 te…

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 p…

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 sayi…

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. Looki…

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, b…

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 toda…

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, …

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 pr…

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 beca…

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 eve…

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 …

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 definit…

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 wa…

> 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, …

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)…