siraben

Thanks, will look into this as another avenue!

Yes, this isn't meant to be a complete port and I only started dipping into mrustc because the previous agents were going off the rails. I have mostly been throwing spare weekly quotas at this but deeper thought will be required to get an actual working Rust compiler in C. Rust is an enormously more complex language, so it might just be at the capability limit.

Specifically the expensive part is getting a C89 port of mrustc to compile rustc 1.90.0. mrustc needs C++ right now, bootstrapping via TCC by writing it in C89 would be the shorter chain.

I am working on this![0] But this is actually a herculean task, I've been chipping at it for weeks and even trying to cheat somewhat by translating mrustc from C++ to C89. If anyone has ideas/cheaper ways to run it I would like to know.

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

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.

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/

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

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

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.

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.

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

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

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

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.

Thanks for the feedback, fixing.

This was made collaboratively by me directing coding agents at the binary, using Ghidra MCP extensively, disassembly and also dynamic analysis with an emulator. I don't have a writeup of the process but it was definitely not fully automatable (I wish though). I might prepare a blog post with transcripts and session history and things I learned along the way.

Broad takeaways:

- Ghidra MCP is not a silver bullet. Lots of opportunities for mis-decoding especially on older instruction sets (e.g. conflating code + data), which requires user input to flag data layout/structs.

- Agents still need a lot of user direction otherwise the RE production is just kind of a random walk. With Z80 it's decent at reading code but I expect that it has much worse performance than reading x86 or ARM for instance. The TI-84+ has a bunch of hardware quirks as well.

- GPT 5.5 is better than Opus 4.8 at RE. Opus 4.8 loves plausible-sounding RE'd logic without any checking. The gold standard is actually dynamically executing the binary and comparing the logic against the prose.

- Maintaining consistency in style and prose is a PITA across the wiki. Hard to reconcile prose <-> code. Can be somewhat mitigated by agent loops.

Was also in discussions with people in the TI calculator programming space who helped provide guidance as well. We previously did not have a catalogue of every subsystem in TI-OS yet alone most subroutines in the OS.

Without installing anything, this can also be reproduced with a shell script that uses a Nix shebang to specify the cross compilers.

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

browsh and carbonyl[0] are such lifesavers on airplane wifi. I find that carbonyl has even better chromium rendering than browsh.

[0] https://github.com/fathyb/carbonyl

See also: https://en.wikipedia.org/wiki/List_of_Germanic_and_Latinate_...

croc's throughput was also a lot better for me. I think this is due to them using multiplexed TCP streams.

Archive link in case it gets taken down: https://archive.is/8MdtL

My favorite aspect of kitty is the infinite scrollback. My scrollback is 10000 lines long and scrollback buffer itself can store 1 GB worth of history.[0] When you hit a certain shortcut, you can use any pager to search through the scrollback. It's all very fast.

[0] https://github.com/siraben/dotfiles/blob/84225d914acd226863e...

I often use jump hosts in SSH, but is the only way to do this in mosh to mosh into the relay and then mosh again?

Fractran is a cool esolang that looks impossible to write any programs in at first until you systematically trace through some examples. A while ago I wrote an assembler in Haskell with an optimizer so you can write programs in assembly-style.

  λ> pretty (sumTo 10)
  c += 0
  n += 10
  while n >= 0 {
    c += n
    n -= 1
  }
  λ> runAssembler (sumTo 10)                      -- Program length: 31
  Right [847425747 % 2,13 % 3,19 % 13,11 % 3,11 % 29,31 % 11,41 % 31,23
  % 11,23 % 47,2279 % 23,59 % 301,59 % 41,67 % 413,329 % 67,61 % 59,73 %
  61,83 % 73,71 % 61,71 % 97,445 % 71,707 % 89,103 % 5353,103 % 83,109 %
  5459,5141 % 109,107 % 103,113 % 749,113 % 19,131 % 113,29 % 131,127 %
  113]
  λ> runAsm (sumTo 10)
  [(Prime 97,55),(Prime 107,1)]

candy waves on a shore: https://tixy.land/?code=sin%28i*t%2F128%29

candy lasers redux: https://tixy.land/?code=0.2%2Bsin%28i*t%2F64%29%2B.3*sin%288...

Replayed it to get a lower time, got 16m 35s.

The crypto prices were so unrealistic. I was able to just keep buying Bitcoin with 2x leverage when it was low and make millions when it subsequently went up after. I barely paid attention to any other ways to make stimulation. Please implement liquidation mechanisms and more volatility.

Yeah it terminates.

A tiny 63 bit program[0] in this language represents a number unfathomably larger than not only ack(9,9), but the far larger Graham’s Number as well. It originates in a Code Golf challenge asking for the “Shortest terminating program whose output size exceeds Graham’s number”, answered by user Patcail and further optimized by user 2014MELO03. With one final optimization applied.

Here's a really short program. Let's calculate 2 * 3

  (λn m s. n (m s)) (λf n. f (f n)) (λf n. f (f (f n)))

eventually it terminates with

   λ s n.s (s (s (s (s (s n)))))

which is just the church encoding of 6.

[0] https://tromp.github.io/blog/2023/11/24/largest-number

Some of the text seems to be cut off, but there is a docx version that loads fine with LibreOffice.[0] I am hosting a PDF export of that too.[1]

[0] https://downloads.reactivemicro.com/Electronics/Reverse%20En...

[1] https://cloud.siraben.dev/s/z9GTFfjDDgGXHSQ

Smooth experience! I loved the details such as the assistant getting a bit annoyed when you go to the vending machine for a drink or “I regret to inform you…” when you try to use the internet terminal on board.