siraben

In the meantime, months ago I achieved bootstrap of TCC (then GCC 4.6) via the same path as the live-bootstrap project but replacing the Scheme part with a C compiler in Ben Lynn's Haskell dialect.[1] This was a project I wish I had time to do years ago[2] but never had the time or motivation for, and the type of things agents can do well now (they couldn't write good Haskell a year ago).

[0] https://github.com/siraben/mrustc/tree/siraben/cmrustc

[1] https://github.com/siraben/blynn-bootstrap

[2] https://logs.guix.gnu.org/bootstrappable/2021-05-26.log#1438...

Comment · 3 months ago

Thank you for the feedback! Will address. Yeah, I intentionally tried to not make the UI too easy to prove things and it shows all possible actions that can be taken from the current point, so that in the future another mode could be added for writing proofs from scratch.

Comment · 3 months ago

I've been working on an interactive click-and-prove prover that is backed by dependently typed terms.[0] The Proof Machine only goes up to some Simply-Typed Lambda Calculus terms, whereas I have the logic sufficiently powerful to support recursion and reasoning about programs and equality.

[0] https://touchproof.siraben.dev/

Comment · 3 months ago

The Z80 was how I learned assembly programming in high school.[0] Was a bit of an unusual choice, but high school students still carry these funky Z80 (or eZ80 now with the color screens) devices every day, so being able to hack on it and have plausible deniability while in class felt great :)

[0] https://github.com/siraben/zkeme80

Comment · 3 months ago

I love traveling with this Anker 160W charger, which has 3 USB-C ports.[0] I just found out about GaN technology last year and I can't believe it isn't more widespread. This one can charge two MacBook Pros and an iPhone at full speed.

[0] https://www.anker.com/products/a2687-anker-prime-charger-160...

Comment · 3 months ago

I use croc instead of magic wormhole as of a year ago now. In my testing the throughput is higher than magic wormhole because it uses multiple TCP connections to transfer the files.

Comment · 3 months ago

This is very cool! I'd like to see a version for theorem proving/equational reasoning as well because I think the ideas behind reasoning about functional programs and proving properties about them are just many cases of rule-applying but people don't staring at equations or jump straight to a theorem prover, whereas a visual interface might make the transition a lot easier.

Comment · 4 months ago

I got a bootable NixOS iso down to 91 MB. Pointed Claude at the Nixpkgs repo and asked it to strip things aggressively and inspect the build closure iteratively.

But the resulting ISO:

- has no network

- can't switch configurations

- doesn't have a text editor

https://gist.github.com/siraben/a8fce9912891d85e1ec3cf74081b...

Comment · 4 months ago

Yes, to type a TI-BASIC program you have to go through the calculator menus which directly insert the tokenized input into the buffer.

The weird thing about TI-BASIC is how seemingly innocent changes in the input can cause huge performance regressions e.g. https://siraben.github.io/ti84p-re/sub-tibasic-for-paren.htm...

  For(I,1,N
  If 0
  1
  End

is much slower than

  For(I,1,N)
  If 0
  1
  End

Comment · 4 months ago

It's highly likely that the original implementation language was assembly. The code is very idiomatic.

Regarding source build, I think reverse engineering it to the point where you can reconstruct the source is possibly legally problematic, so I don't plan to do this, but maybe for certain subsystems like MathPrint (equation display) which was especially fun to RE. I have a PR up for it and it will be live at

https://siraben.github.io/ti84p-re/mathprint

Comment · 4 months ago

The plans are heavily subsidized by the AI companies so I didn't end up needing to do API usage or buy another subscription. I have ChatGPT Pro and Claude Code Max.

Comment · 4 months ago

Thanks for the feedback, fixing.