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