ianhorn

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, but it's a big benefit to have stronger compiler guarantees of correctness so that an LLM can't screw things up as much. No BSing that it works when the compiler requires proof.

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 that code has third party dependencies that would be terrible to give up. It's totally unclear right now how to get the best of both worlds.

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 for a function that amounts to "take a Foo x and return a Bar y with a proof of does_what_i_wanted(x,y)." Voila, no more agents doing something else because it won't compile if they don't do what I wanted.

It's great to build faster without the frustration of having no confidence in what I build. But it sure makes the gap between toys in Lean and using this in a Real Project in some other language that much more frustrating.

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 the “interactive” part makes it a combo of IDE and language and they seem to get pretty tightly coupled in practice. You can’t talk about the language without talking about the environment you use it in.

I’m not the biggest VS code fan, but a battle honed extensible IDE used by zillions and maintained by $$$ has proved itself miles ahead of the environments for alternatives. As far as i can tell, the excellent onboarding path that is the Natural Numbers Game is possible because of VS code’s hackability and ecosystem.

My main concern as I’m learning lean is that the syntax extensibility seems to be a double edged sword. Once i’ve learned a language, i want to be able to read code written in it. If everything is in a project’s own DSL, that can get out of hand, but that comes down to community/ecosystem so i’m crossing my fingers.

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 so frustrated by these things right now.

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 generalizable language helps us use and reuse them better, and that (like programming language evolution) we're always finding new ways to express problems precisely. Reusability of ideas and solutions is great, but sometimes the "language" gets in the way, whether that's a programming language or a particular shape of the formal expression of something.

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 people have been complaining that the measures that get touted in political discourse don't reflect quality of life. So if we stop looking at those as measures because they cease to be reliable, maybe they stop getting myopically optimized and we can get less myopic about what we prioritize in aggregate.

But looking at the second one, I've also wondered whether those measures really do reflect typical quality of life, and it's just that the people doing worse than typical will always see the measure as the wrong measure. So then we'd be losing the ability to prioritize actually useful things.

In my heart though, I kinda lean towards the first one. I've been in enough orgs where "the dashboard goes up" is incentivized to the detriment of the unmeasurable things that actually matter to the org.

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 limit definition of pushforwards. Never found a nice way to swap which is primary and which is secondary, but it feels like there should be a clean view of it that way somewhere.

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 like "Scholars believe that professional competence of a teacher is a prerequisite for improving the quality of the educational process in preschools" be put in a lean-like language?

Totally out of scope in the any near future for me at least. But that doesn't prevent it from being super useful for a narrower scope. For example:

- How might we take a statement like "(x + 1) (x - 5) = 0" and encode it formally?

- Or "(X X^T)^-1 X Y = B"?

- Or "6 Fe_2 + 3 H_2 O -> ?"?

We can't really do this for a huge swath of pretty narrow applied problems. In the first, what kind of thing is X? Is it an element of an algebraically closed field? In the second, are those matrices of real numbers? In the third, is that 6 times F times e_2 or 6 2-element iron molecules?

We can't formally interpret those as written, but you and I can easily tell what's meant. Meanwhile, current ways of formally writing those things up is a massive pain in the ass. Anything with a decent amount of common sense can tell you what is probably meant formally. We know that we can't have an algorithm that's right 100% of the time for a lot of relevant things, but 99.99% is pretty useful. If clippy says 'these look like matrices, right?' and is almost always right, then it's almost always saving you lots of time and letting lots more people benefit from formal methods with a much lower barrier to entry.

From there, it's easy to imagine coverage and accuracy of formalizable statements going up and up and up until so much is automated that it looks kinda like 'chatting about real-life statements' again. I doubt that's the path, but from a 'make existing useful formal methods super accessible' lens it doesn't have to be.

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.github.io/assets/cv.pdf) Machine Learning Engineer with over a decade of industry experience in ML, stats, and numerical optimization roles. Looking for companies where ML is critical path, especially in NLP.

Email: horn (dot) imh (at) gmail

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 cool. I’d bet it’s not too long ago that this would have to be something you’re seriously pursuing to make the costs worth it. [0]

Or if we’re sticking with tech = computers, I can sculpt for free in blender (the software) and print it with a 3d printer. Or paint in procreate/photoshop on my ipad with this fantastic not-really-a-pencil (and somehow procreate is only $10??). Or learn to draw from the internet.

Or the fact that nothing like D&D Beyond existed for a game I’m playing, so I was able to put up an app based on free software (react + yjs) on cloud servers god knows where for dirt cheap without knowing much of anything about any of those things.

Hobbies and leisure activities seem to be pretty accessible (in price). The downside for me is that all the accessible addictive stuff (like this site) makes it hard to actually dedicate time to the hobbies I want to spend time on.

[0] Unfortunately, I couldn’t find data on prices of various art supplies going very far back.

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 are also whole classes of error you do make that you wouldn’t make in normal programming).

I have been using it for character sheets in tabletop RPGs I’m playing lately, and it’s great. With a line of js, you can add an arbitrary button to google sheets, and then it turns into a quick, dirty UI that’s transparent (click on the cell and see that AC=10 plus dexterity modifier) and on-the-fly editable by everyone together.

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 use their training data.

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 addressed in here: input methods strongly affect the medium.

Last year I struggled intensely with RSI. I got to the point where I couldn’t type for months. I tried some voice coding tools (caster and talon). Some aspects of this were actually better than keyboard coding. Unfortunately speech recognition is still at a point where it drove me insane with inaccuracies.

It also made me realize that with a keyboard, text code is incredibly natural. With keyboard+mouse, some new modes open up. With voice alone, I wanted to code a very different way.

I won’t go into detail, because this is already a long comment, but I believe that when we get speech recognition as reliable as typing, we’ll see an explosion of new programming paradigms.

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 correlated, while A doesn't cause B (or neither causes the other), and while their definitions have nothing to do with each other. Like nurse and gender. They're correlated in the US, but making someone a nurse doesn't change their gender, and the definitions have nothing to do with each other. Maybe in some countries the correlation is even flipped!

Recall all the times in stats where an estimator can be an unbiased estimator of a correlation while being a biased estimator of a causal effect.

So you get some people saying it (the correlation) is correct and other people saying it (the causal effect) is incorrect. Both are right! To stop talking past each other, they need to talk about bias with respect to the correlation or bias with respect to the causal effect in this particular direction.

But what frustrates me is when the correlation side uses the (true) correlation to argue against a system being biased with regards to something else (w.r.t. a definition or w.r.t. a causal effect or w.r.t. a literal translation or w.r.t. some more complicated aspect of the system), and that harms are okay because the bias is a correct bias.

We need to work on our terminology so that we can stop talking past each other. It doesn't help that our models have weird biases in absurdly complex function spaces, but we have to progress beyond a first-stats-course one-size-fits-all definition of bias.

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 update does not to fix. A fairer comparison regarding readability would be pulling out the matrix version of a into a named variable:

  n = len(a)
  A = a.reshape(n,1)
  M = exp(1j * k * sqrt(A**2 + A.T**2))

When you need loops, you need loops, of course, and python tends to suck here (though with jax's functional programming constructs the boundary is shifting). But the readability/cleanliness comparison in your post is still an unfair comparison.

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 option. If you mean a single numeric type, like javascript, it unfortunately leads to a bunch of issues. Integers and floats really are both necessary very frequently. For example floats to represent something like speed, and ints to represent your bank balance. And you need different sizes of them (like float32 vs float64) are still necessary in a ton of applications, so you'll need them eventually if you want the language/numerics library to be truly general purpose.

It's also a huge convenience to be able to apply e.g. `+` to arrays as well as numbers and other polymorphism niceties.

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/drive/1ABrZJlm8pwB6_Sd6ayO...

On my macbook, using XLA's jit in python gave about a 12-15x speedup on CPU over OP's solution, which was pretty cool, but I'm too lazy to figure out how to install and benchmark Julia on my machine. Applying a 12-15x speedup would at least beat the Julia MT solution in OP, and you've got to admit `exp(CONST * sqrt(A**2 + A.T**2))` is a pretty clean way to do it.

Then I ran on whatever GPU colab decided to give me (a P100), and for just adding a decorator, it's a 1000x-1900x speedup (better as n goes up). Hence my current honeymoon period with jax. I love the speed vs readability tradeoff.

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 numpy as np` for `from numpy import newaxis, exp, sqrt`, then IMO, the numpy is more readable:

    A = a[newaxis]
    M = exp(1j * k * sqrt(A**2 + A.T**2)) 

Side note: any idea why the python and fortran are exp(i k... while the julia is exp((100 +i) i...)? Is it something I overlooked?

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

    n = len(a)
    A = np.tile(a,(n,1))
    A_T = np.tile(a.reshape(n,1),(1,n))
    M = np.exp(1j*k*(A**2 + A_T**2))

    n = len(a)
    A = np.tile(a,(n,1))
    M = np.exp(1j*k*(A**2 + A.T**2))

    A = a[:, np.newaxis]
    M = np.exp(1j*k*(A**2 + A.T**2))

    A = a[:, np.newaxis]
    M = np.exp(1j*k*np.sqrt(A**2 + A.T**2))

    A = a[:, np.newaxis]
    root_sum_squares = np.sqrt(A**2 + A.T**2)
    M = np.exp(1j*k*root_sum_squares)

--------

And to pitch the hype train for jax: if you want to fuse the loops and/or get gpu/tpu for free, just swap np for jnp:

    A = a[:, jnp.newaxis]
    M = jnp.exp(1j*k*jnp.sqrt(A**2 + A.T**2))

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, even as an R user. Doing it with a web stack would be more appropriate, but even then it would have been a lot more work and I can't think how I'd do it without spinning up a server and setting up some http endpoints.

People are all talking about how it's useful for quick stuff with datasets, but it goes far beyond that. It's useful for quick anything you might want a small database for. Imagination is the limit.

For example, if any of you play D&D online, you might be familiar with dndbeyond's character sheets. They're a fantastic way to onboard new players who might not have the inclination to spend hours with the rule books before they even start playing. It does all the calculations for you and gives you some buttons like "roll athletics" and doesn't let you add more spells than your character can have with their stats.

I recently persuaded some friends to give FATE a try and built analogous push-button character sheets with google sheets [0]. It was quick and simple. With conditional formatting, you highlight bad states (rules say you can't have more of X than Y!). With the script editor, you can add full on buttons for dice rolls and other state changes with whatever logic you want (anything you can code up!). Checkboxes are obvious but super useful. And the transparency of the calculations is helpful for teaching people the system (this stat is "min(A4, B1+C5)").

Without google sheets, it would be a serious endeavor to build a stateful, database backed, live collaborative GUI that can be added to and customized on the fly by my users. With google sheets, it was a quick fun afternoon hack. Excel/google sheets is an amazing piece of technology.

[0] Screenshot of the "app": https://raw.githubusercontent.com/imh/public_images/main/Scr...

Most ceiling fixtures have a couple bulbs. Get one with three, and a bedside table + lamp on each side of the bed. That’s at least five hue bulbs, which lights up a room very effectively. Not full sunlight, but enough.

I think you aren’t including in your calcs that you’re presumably not in a black room. A light colored paint means the light that isn’t going straight to your eyes from the bulb still brightens the room significantly.

I have a Hue light on my bedside table that goes from 0 to max over 30min, plus three bulbs in the ceiling socket that do the same, but are staggered. Like bedside can be 6:55-7:25, with overhead 1 from 7-7:30, overhead 2 from 7:05-7:35, etc. So you have the four lights brightening together over the course of 45min or whatever longer period you want.

If it's gradual enough, you won't just bury your head, and if it's enough bulbs, it'll get bright enough to convince your body it's daytime.

There's another trick I've been meaning to do. The Hue app's wake up routine turns it on to a low temperature light, but turning it a little higher temp/bluer once I'm up does help trick me into daytime. I'm meaning to make a cron job on my raspberry pi to make my own wakeup routine that is a little slower to avoid the need to stagger lights, and also increase temperature once it's bright. If you know linux, the pi is easy.

Even without the fancy pi stuff, it's Good Enough. The Hue bulbs add up fast in cost, but it's worth it to me. I have the white ambiance ones.