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.

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’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.

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

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.

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

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

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.

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.

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

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.