ianhorn

6 ms·

1.
by ianhorn 18d ago
That’s practically what i’m working on! But i’m training the models to do this natively. It gets complex given the inherent relevant uncertainties (aka making it resilient to their bullshit). Luckily, datalog and monotonic logic in general
2.
by ianhorn 27d ago
I'm working on a bidirectional version of this! The big challenge is keeping the various versions of the thing in sync through edits.
3.
by ianhorn 2mo ago
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 the second language is as mainstream as it gets in
4.
by ianhorn 4mo ago
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&#x27
5.
by ianhorn 4mo ago
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 guarantees on, and t
6.
by ianhorn 4mo ago
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 signature
7.
by ianhorn 5mo ago
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 is that th
8.
by ianhorn 5mo ago
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.
9.
by ianhorn 5mo ago
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 rai
10.
by ianhorn 6mo ago
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 reusable genera
11.
by ianhorn 6mo ago
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?
12.
by ianhorn 6mo ago
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 people have been complain
13.
by ianhorn 2y ago
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 in terms of the l
14.
by ianhorn 2y ago
Any chance you know of good DAE books/resources that go into combining symbolics and numerics or parametrized DAEs?
15.
by ianhorn 2y ago
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 like &q
16.
by ianhorn 4y ago
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 ( https://imh.gi
17.
by ianhorn 5y ago
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 dinner out, which is so c
18.
by ianhorn 5y ago
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 state all together (there
19.
by ianhorn 5y ago
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 license at all to
21.
by ianhorn 5y ago
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 addressed in here: i
22.
by ianhorn 5y ago
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.
23.
by ianhorn 5y ago
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 correlated, whil
24.
by ianhorn 5y ago
It wouldn't be a smooth app, but it would still render, which would be fun to play with.
25.
by ianhorn 5y ago
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 update does
26.
by ianhorn 5y ago
> 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 great o
27.
by ianhorn 5y ago
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): https://colab.research.google.com
28.
by ianhorn 5y ago
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 `import nump
29.
by ianhorn 5y ago
This an unfair example of trying to make the numpy readable: n = len(a) M = np.exp(1j*k*(np.tile(a,(n,1))**2 + np.tile(a.reshape(n,1),(1,n))**2)) This has a common issue in functional programming and there's an easy trick
30.
by ianhorn 6y ago
Grandparent here. Yeah I know how to program, but the point here was to make my players a simple interactive GUI that saves its data somewhere we can all access together (e.g. the cloud). Doing that in R would be well beyond my skillset, ev

More ›