> But on your right side, you have turns: the expression cos x + i sin x is literally saying that the point whose angle is x on the unit circle in the complex plane is the complex number .

I totally agree here, and that's purely geometric, regardless of what we express x in. We can talk in terms of abstract points without specific coordinates/embeddings in R.

> When you have that 2π in there, but not in the sin and cos expressions, you're using different angles for multiplication/exponentiation and for sin/cos.

This part I'm not following. When we talk about a scale, any purely universal identity like Arg(z^2) = 2 Arg(z) is going to hold regardless of the scale. I agree that the Arg stuff nicely motivates interpreting it as an angle, but don't see how it says anything at all about the scale in question. Like, we get an interpretation of e^2πix as working in angles from the Arg reasoning, but we don't get a scale for those angles from it, do we? We'd only get Arg if we impose a scale on Arg itself, right?

So if we take e^2πix at x=1/2 turn=1/2, we get e^πi=-1, which gets us Arg(-1)=1/2 turn=pi rads=180 degrees, and we can work from there, but I still don't see how it imposes a unique scale that we can say is still radians and thus incompatible with the RHS's scale of turns.

If we want to get real interesting with it, this could also motivate an explicitly geometric "unit" aware exp operation, and depending on the defaults we use for the angular scale and the linear scale, 2 pi could be the conversion factor, making exp(2 pi i x) = cos x + i sin x actually interesting and useful and clarifying.

[0] pedantically, they're not units, or at least not dimensional units, so whatever the word for dimensionless units are, as in degrees vs radians vs turns.

Like, if you meant "the correct program" in a sense where two pure total functions can be different despite both having the same outputs on the same inputs, then that's not what I'm responding to.

And yeah I know prolog, but proof assistants and logic programming are totally different beasts. Definitely not copy/pastable to/from lean, at least as I've seen and used each.

> Or are you saying that the program has to be the efficient implementation? Because that’s a different ball game. I’m not even going to get into how you could provably transform brute force propositional logic into efficient algorithms. (At that point we’ll have finally created the fabled “sufficiently smart compiler” and probably solved p=np).

I think you're totally misunderstanding. What I'm saying is that in something like Lean (just because I know it best) I can say, "this function takes inputs satisfying Prop1 and returns outputs satisfying Prop2," in ways where I write some brute-force equivalent formalization of Prop1 and Prop2 in the most straightforward way, and then go on to prove that they are true of my program that is not the brute force implementation. Like the wacky famous magical inverse square root implementation from Quake III. You could write a spec that "output = 1/sqrt(input) up to float properties" and the implementation in the famous brainfuckery way. To your comment about how the spec is as hard as the implementation, "output = 1/sqrt(input)" is way easier than the weird efficient implementation, and that class of distinction is super common.

And as you said, the annoying part is showing that the efficient implementation satisfies the spec, but what's magic today is that we have great tools and LLMs can and do fill in the blanks. In practice, I write the spec by hand for the stuff I care about and then prompt the rest and know that my spec is what the LLM implemented.

> > The magic is that you can write a spec that's clear

> Maybe you can. But I did spend a grad class with rocq (coq at the time) and a decade working with “systems engineers” and am not convinced that this is a realistic expectation.

I tried rocq back when it was coq too, and now do most of my work in lean and rust and python with totally normal folks and I'm convinced that the tooling and languages are finally just about Good Enough. If you have any interest in the field, which it sounds like you do, and if you haven't checked out the ecosystem in the last couple years, I'd recommend you check it out again.

That's not remotely true. Or, more formally speaking since we're in a thread about proof assistants, it's not remotely true, up to extensional equality, plus some choices about which axioms you use.

I can write a formal description of what it means to have property in a way that does have computational content that is equivalent to an algorithm[0], but often the clearest way to express the property is equivalent to an algorithm that literally brute forces the problem, like sorting a thing by checking every permutation until you find one that's sorted.

The magic is that you can write a spec that's clear, then have the LLM write the code and prove the spec, so you know that given the right inputs/state, it will return the right outputs/state. Then the gap is performance-like characteristics, which is a pretty great starting point and a lot easier to be just empirical about than correctness.

[0] in Lean you can also use classical logic or add your own axioms, where it's not even comutational.

The one that I remember most strongly that way was the unique mapping from the empty set/object/whatever as a theorem.

I guess it’s the fact that Anthropic usually frame this around morality and risk to society that makes it different. Instead of “risk/harm to me vs reward to me,” their framing reads as “risk/harm to us vs reward to me” or “immorality vs reward to me.” That’s what makes it feel like a great metaphor.

The standard cost benefit analysis we all do justifies increasing the harm to others if the opportunity to benefit ourselves goes up.

Imagine two parallel universes:

- in one, you take ten minutes to make a dashboard that shows management what they asked for. It passes code review before merge and the exec who asked for it says it's what they wanted.

- in the other, you take a day or two to make it. Again, it passes code review before merge and the exec who asked for it says it's what they wanted.

Which version of you is more likely to get positive versus negative feedback? Even if the quick-to-build version isn't actually correct? If you're too slow and aren't doing enough that looks correct, you'll be held accountable. But if you're fast and do things that look correct but aren't, you won't be held accountable. You'll only be held accountable for incorrect work if the incorrectness is observed, which is rarer and rarer with fewer and fewer people directly observing anything.

So oddly, with nobody doing it on purpose, people get held accountable specifically for building things the way you're advocating.

I imagine that orgs that do lots of incorrect work could be outcompeted but won't be, because observability is hard and the "not get in trouble" move is to just not look too hard at what you're doing and move to the next ticket.

What I do mourn is the reliability. We're in this weird limbo where it's like rolling a die for every piece of work. If it comes up 1-5, I would have been better off implementing it myself. If it comes up 6, it'll get it done orders of magnitude faster than doing it by hand. Since the overall speedup is worthwhile, I have to try it every time, even if most of the time it fails. And of course it's a moving target, so I have to keep trying the things that failed yesterday because today's models are more capable.

Doing the verification after the execution tends to lead to “yeah this is good” when it really isn’t. Stuff like copilot annoyingly loves to change the tests so it can pass, rather than changing the implementation to make the tests pass. I wonder if their platform prevents that kind of thing.

Some differing interpretations of the law distinguish between the lawmakers' intention vs the literal meaning (and keep in mind that language itself changes a lot in just a few centuries. The hard problem is that, in PL terms, the law is written in syntax without agreed upon semantics. So a decent step could be just using some agreed upon semantics, like we do in code! Then at least "interpreting" it would be unambiguous.

Maybe a decent analogy would be gcc vs clang might produce different programs for certain undefined behavior, and different combinations of pieces might lead to different behavior too (like race conditions), and somebody (the plaintiff/user) is asking you (the judge/compiler) to decide what's going to happen in this next loop/program/whatever.

Or maybe a decent analogy would be getting a ticket that the API is erroring in some rare user's case and having to look into the code and stacktrace to realize it's some weird unanticipated interaction between two different pieces of legacy code (150 year old law) that now interact due to a recent merge (a new law from last year), and now it's crashing, so we have to figure out how to interpret/compile/resolve this user's case.

If law was usable like code, we'd never have any of those issues, just like we never have those issues with actual literal programs. And when we do, it's just because we're using the wrong language/aren't encoding enough things in the types and semantics/shouldn't have used this niche compiler so now let's get a new interpretation from another Supreme Compiler/etc. Life would be easier \s

So it's maybe more optimistic than you, in that the run/read time power (judicial) doesn't get diminished, but more pessimistic in that I believe it because I believe that changing the language from english law jargon to some formal language doesn't actually eliminate the issues it might be intended to eliminate.

The example I gave had a few pieces:

- x is defined prior to the if/else, and overwritten in just one branch - y is defined in both branches

So in the rest of the function, we have both x and y available, regardless of which branch is taken.

I just took a quick read of the context page and the context basics page, but it's still unclear to me whether you can program how scopes/contexts interact in rye.

In my example, we I'd say we have a few different scopes worth mentioning, and I'm curious how programmably we can make them interact in rye:

Scope 1. Right below the first x = ...: we have names available form and have x available as the ... stuff. Presumably the `foo` in `if foo` lives in this scope.

Scope 2T. Right after the true branch's y, we have scope 1 plus y introduced

Scope 2F. Right after the false branch's x and y, we have scope 1 plus x "pointing to" something new and y introduced.

Scope 3. Below the if/else, where lives. This is either scope 2T or scope 2F. x is either scope 1's x or scope 2F's x, and y is either scope 2T's y or 2F's y.

In the original articles language,

So the scope relationships in an if/else are a diamond DAG taking the names from before it, making them available in each branch's scopes, and then making a sorta disjoint union of the branch's names available afterwards. Could that be programmed in rye, to allow the kinds of naming ergonomics in my previous example, but with the if/else being programmable in the sense of the original article? I'm especially interested in whether we could overload it in the traditional autodiff sense.

Responding to a different part of your comment about using names rarely in rye, I've found that I benefit a ton from handing out names more than most people do in functional languages, just for clarity and more self-documenting code. Like, the ide can say "`apples` is broken" instead of "error in location xyz" and I can rebuild my mental state better too when revisiting code.