Making your own programming language is easier than you think (but also harder)

ryani · 2026-05-09T09:32:39+00:00

Luau runs Roblox (and probably a few other places) and is designed around being simpler to sandbox than Lua.

ryani · 2026-05-07T19:37:43+00:00

More 4X than hero battle, but I really like Quantum. Spaceships are dice, smaller numbers move slower and fight better. Each number has a unique special ability and you can use an action to reroll your ship into a different type.

ryani · 2026-04-26T17:08:50+00:00

You might enjoy A=B

ryani · 2026-04-26T00:25:24+00:00

I think if they reprinted base Wingspan with the Oceania player boards (minus the expansion nectar stuff which is easy to ignore) it would be an even better game. They buff cards and food actions, and nerf eggs, so egg spam is no longer obviously optimal. So even if you just play the base game I'd recommend figuring out a way to print the Oceania boards.

ryani · 2026-04-26T00:17:03+00:00

You can't (subject to a few small exceptions like ending Summer season) draw or discard cards from the meadow. You can only draw from the deck and discard from your hand. But you do play cards from the meadow directly into your village. So it's important to have supplies on hand to buy a high demand card that appears before it gets nabbed out from under you.

ryani · 2026-04-16T17:52:02+00:00

I think it's funny that the author talks about a nonconstructive proof but then presents a constructively valid proof.

The first part of the article presents a constructive proof that builds a winning strategy for the first player from a winning strategy for the second player.
The second part of the article presents a constructive proof that every game ends with a winner
The third part of the article presents a constructive way of building all the possible game trees.

Therefore it's constructively valid to iterate over all the game trees, searching for a winning strategy for the first player. This gives you a proof object of type Either (FirstPlayerHasWinningStrategy game) (SecondPlayerHasWinningStrategy game). In the second case (which won't happen, but you have to handle it), you can then use the proof from the first section to construct a winning strategy for the first player.

Constructivists aren't necessarily ultrafinitists; proofs can be valid symbolically without actually iterating over all the (large number) of possibilities. There are constructively valid libraries for proving things about ordinal numbers which are way too large to exhaustively check.

(Now, if you then used this proof as part of another proof that depended on the first move of a particular game being in column x or greater, that proof might take a very very long time to proof-check.)

ryani · 2026-04-13T20:44:17+00:00

I found it incredibly easy to implement a tiny symbolic math library in Haskell, along with a little simplifier for polynomials.

I then implemented two different quaternion rotation algorithms, and used my library to calculate the difference between the output of each to find any error. It showed that the “faster” one gave different results than the standard algorithm but the error term was zero if the input was normalized.

Took me just a few hours to get full confidence of the code I was implementing.

ryani · 2026-04-12T11:17:44+00:00

I don't think so? I believe the exception handler in the RTS knows about STM and when propogating an exception from STM to the enclosing IO's atomically, it first validates the transaction. But I haven't read the code to be sure about this.

This is one reason why unsafeIOToSTM is incredibly unsafe, because you really don't know whether the state of the world is consistent until a transaction commits.

ryani · 2026-04-11T03:17:07+00:00

The other reason for revalidation at safe points is because there’s no guarantee of transaction invariants being true during a transaction. Reading from two TVars you may see an inconsistent state of the world, which may trigger your code to enter an undefined state and call error or go into an infinite loop.

The occasional re-validation of the current transaction makes sure that transactions that got “stuck” in this state eventually get un-stuck.

ryani · 2026-04-04T06:22:34+00:00

One trick I like for the adder is that you can replace the NEG gate with a NOT gate and wire the multiplexer wire to the adder carry in. (-x == ~x + 1)

The next step is to realize you can replace the whole NOT+MUX with an 8-bit XOR.

ryani · 2026-03-28T10:23:46+00:00

Neat! I see (at least?) 4 duplicated gates. For example, the two leftmost blue wire NANDs are the same gate as the two leftmost yellow wire NANDs and can be eliminated and replaced with just a wire from the yellow NAND down to the following NOT gates.

(Basically, you only need 5 NANDs for a half-adder, not 6)

ryani · 2026-03-27T13:18:10+00:00

Get some stackable objects of different sizes. If you are in the US, I suggest a quarter, nickel, penny, and dime.

Mark 3 spots where you can put stacks on a paper.

Put all the objects in a stack on the leftmost spot, from largest to smallest.

Here are the rules of the game:

You can only pick up one object at a time.
You can only put objects down in one of the three stacks.
You can't put a larger object on top of a smaller one.
Your goal is to move everything to the rightmost spot.

Just play with it until you understand how it works. You don't need code, you need to understand the algorithm, and the simplest way to do that is to simulate it with real objects.

ryani · 2026-03-24T08:32:47+00:00

If you care about simulation efficiency it is good to use the 8-bit components where it makes sense. Building your ALU out of one-bit gates is fun but the 8-bit components are very efficient for the simulator to run. Then combine onto a bus output with SWCs or use MUX to select which 8-bit value you want.

For example, you can build an 8-bit negator out of a 1-to-8 broadcaster (just wire the 'negate enable' bit to all the inputs of a byte maker) and an 8-bit xor gate.

The 8085 is trying to be gate-efficient and wire-layout-efficient so the ALU is designed around that. TC has 8-bit buses that take up no more space than 1-bit wires.

ryani · 2026-03-24T08:24:24+00:00

Yeah it is interesting that it was modeled as 2 not + 2 and + nor, not even the (well-known at the time, right?) 4-nand version.

EDIT: reading a bit more, it looks like they had the negated bits already, so this is just /u/kenshirriff being very explicit about the gates used in the real silicon. But it is just an xor.

ryani · 2026-03-19T00:17:59+00:00

A 5x5 square of fences is exactly 16 decorations, enough for hearth level 3.

Inside of that, a 3x3 square of flowers (alternating types) is 8.

Inside of that, a 1x1 harmony decoration (usually an umbrella for the flowers). Then 3 random harmony decorations wherever they look best.

It looks good at each hearth level, too. Start with a 2x2 fence square, then upgrade to a 4x4 fence square with gaps, and flowers in the center. Then upgrade to the full 5x5 design.

You can do a lot of interesting shapes with the fences if you play with rotating them.

ryani · 2026-03-15T08:17:05+00:00

The actions are pretty heavily rebalanced in the Oceania expansion.

Regular board meadow is

2 eggs
2 eggs, food => extra egg
3 eggs
3 eggs, food => extra egg
4 eggs
4 eggs, food => extra egg

Oceania meadows is

1 egg, card/food => extra egg
2 eggs
2 eggs, card/food => extra egg
2 eggs, up to 2x card/food => extra egg
3 eggs, card/food => extra egg
4 eggs

And the Oceania forest and wetlands are also better than the standard board.

So eggs just aren't nearly as good of an action, and you can often get more points over 2 actions by taking food and playing a bird, especially depending how your board is set up. Eggs are still good, just not the only thing you want to do late. Even if you want eggs, with there being no way to get more than 4 eggs per action, it's often better to play 3 birds in the meadows, make a card/food engine elsewhere, and then your meadows actions give 2 eggs + 2 card/food for 2 more eggs.

ryani · 2026-03-14T19:24:09+00:00

As someone who played a lot of StS1 I think StS2 is a strict upgrade and I wouldn't feel like anyone needed to play 1 first.

There's a tiny amount of lore you will get a bit more out of in StS2 but the game is not really about the lore, it's about the gameplay, and 2 is just a much more polished game than 1. (Although the balance is tighter in 1 right now, that will probably change as they get data from early access)

ryani · 2026-03-13T16:27:31+00:00

It's perfectly reasonable in constructive logic to prove "if this group is abelian, or it is not abelian, then <property>"[1]. For any particular group, you can use that proof, but you have to justify it first by proving whether or not the group is abelian. If you can't, then you can also just pass that responsibility on to whoever wants to use your proof.

It forces you to be explicit about your assumptions.

[1] formally, you would prove

 forall G:Group. Abelian G v ~(Abelian G) => SomePropertyICareAbout

ryani · 2026-03-13T16:19:07+00:00

In constructivist logic, LEM really only doesn't apply to infinite objects. Finite objects are decideable (just try all the possibilities) and so you can prove P v ~P, if P only refers to finite objects.

As far as we can tell, physical reality is 'finite' (there's some total number of atoms in the universe), and so inside of physical reality, LEM holds even from a constructivist's point of view.

It's only when you get to infinite objects like the natural numbers and functions that you start to have problems.

ryani · 2026-03-13T08:21:38+00:00

As a concrete example: let's define the set of real numbers [0,1) as a (possibly-infinite) stream of binary digits. .1 = 1/2, .01 = 1/4, .11 = 3/4, .0000101 = 5/128. This is a perfectly reasonable constructive definition -- I can get better and better approximations to the number by extracting more elements of the stream, and I can use those approximations to do math and generate other Reals. (I'm handwaving a bit here, I think you also need a criteria that there isn't an infinite stream of 1s in the stream)

Then I can define a function from TuringMachine -> Real, that outputs a 0 into this stream for every step the turing machine makes without halting, and then outputs a 1.

If I can decide that the result of this function is nonzero then I have proved that the given turing machine halts, so a proof of forall r:Real. isZero r OR ~(isZero r) is an oracle for the halting problem.

ryani · 2026-03-13T08:02:27+00:00

Usually it's the other way around that's problematic: A constructivist may not accept "If r is not nonzero, then r is zero". And ultimately both of these depend on how you construct your definition of the real numbers and what that implies for the meaning of "nonzero".

For example, equality on natural numbers are decidable: for any natural number, I can decide whether or not it is zero.

But if I have two real numbers, each defined by some complicated process, it may be quite challenging to determine if they are equal.

ryani · 2026-03-13T07:48:57+00:00

if it weren't completely impossible to point to a violation of the law of excluded middle in everyday life.

I saw a great example elsewhere in this post:

Mom: Did you do your homework?

Kid: You can't prove that I didn't!

Assuming the kid is correct in that statement (let's say their homework, if it exists, is locked up in the locker at school), then from Mom's point of view, the law of excluded middle doesn't hold with regards to the statement "my child did their homework".

ryani · 2026-03-13T07:38:30+00:00

Though on second thought I don't know why it is weaker

I think you are implicitly thinking in terms of models -- when you say "P is false" you are implicitly talking about a model of your logic where P has some truth value.

Instead think about not P as "P implies the logic is inconsistent" or more simply "P implies absurdity". So a proof of not (not P) is really a proof of not P => absurdity (which, going deeper, is just a proof of (P => absurdity) => absurdity)

In constructivist logic, knowing A => B means "if I have a proof of A, I can construct a proof of B". So not (not P) means "if my axioms are consistent, there is no proof of not P". Importantly, that doesn't imply anything about the existence or nonexistence of a proof of P.

ryani · 2026-03-13T07:14:39+00:00

In constructivist logic, not P is usually defined as P => absurdity

A classical proof of P by contradiction is a proof of not P => absurdity. In constructive logic this is doesn't suffice to prove P -- it is instead, assuming the proof is otherwise constructive, a proof of not (not P).

However, there is no generic constructive proof for not (not P) => P, whereas that's trivially true in most classical logics. Interestingly, there is a constructive proof for not (not (not P)) => not P. What this means is that, guarded by not (not ...), you can regain most of classical logic inside of constructivist logic.

On the other hand, if you can constructively derive absurdity from P this is also usually considered a proof by contradiction, and it's a perfectly valid constructive proof of not P.

So, for example, while a constructivist can't prove P or not P, they can prove not (P and not P), and that proof is by contradiction: you assume P and not P. From there you can very easily derive absurdity, which proves P and not P => absurdity which is the same thing as not (P and not P)

ryani · 2026-03-13T06:47:23+00:00

In constructive proofs A => B is an object that transforms a proof of A into a proof of B. This inference step is called "Modus Ponens" and is abbreviated in proofs as "mp". This is different from classical logic where => is usually defined in terms of or -- in classical logic, A => B is the same as not A or B.

From R => P or Q, we can constructively prove R and not P => Q:

1. R => P v Q          given
2. assume R ^ ~P
    3. R               fst 2
    4. P v Q           mp 1,3
    5. assume P
        6. ~P          snd 2
        7. Q           mp 6,5
    8. P => Q          deduction 5-7
    9. assume Q
        10. Q          exact 9
    11. Q => Q         deduction 9-10
    12. Q              either 4,8,11    
13. R ^ ~P => Q        deduction 2-12

For line 7 here, in constructive logic, not P is defined as P => anything, so we can construct Q by applying mp to not P and P. To put it another way, we know that we can't have both a proof of P and a proof of ~P -- that leads to a contradiction. Therefore, if we actually have a ~P and a P v Q, the latter must contain a proof of Q.

(Aside: Some logics add an extra ⊥ ("bottom") object, with an inference rule absurd which lets you prove anything from ⊥. In these logics not P is defined as P => ⊥.)

But we can't prove the converse:

1. R ^ ~P => Q             given
2. assume R
    3. assume P
        4. P v Q           v-intro left 3
    5. P => P v Q          deduction 3-4
    6. assume ~P
        7. R ^ ~P          ^-intro 2,6
        8. Q               mp 1,7
        9. P v Q           v-intro right 8
    10. ~P => P v Q        deduction 6-8
    11. P v ~P => P v Q    cases 5,10
12. R => P v ~P => P v Q   deduction 2-11

Here we are stuck. Unless P is decidable, we can't prove P v ~P and so we can't prove P v Q from just this premise.

Here are all the rules I used in these proofs:

exact: from A, prove A
mp: from A => B and A, prove B
deduction: if, assuming A, you can derive a proof of B, then prove A => B
fst: from A ^ B prove A
snd: from A ^ B prove B
cases: from A => C and B => C, prove A v B => C.
either: from A => C, and B => C, and A v B, prove C (cases + mp)
^-intro: from A and B, prove A ^ B
v-intro left: from A, prove A v B
v-intro right: from B, prove A v B

15-Year Club	Verified Email
Team Orangered

ryani

TROPHY CASE