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?
Great question. Matt has a comment about this here, and he has an actual PhD on the subject! So rather than doing a worse job explaining I will leave it to him to explain: https://news.ycombinator.com/user?id=mweidner
- 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.
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.
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.
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.
reply