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).
> If anyone has ideas/cheaper ways to run it I would like to know
GCC 4.7.4 was the last version of GCC fully written in C, with full C++98/03 support and a decent subset of C++11. As far as I know it is used by the bootstrap project presented in the article.
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.
Sounds pretty difficult (if not impossible, see cfront 4.0) to translate C++ code to C89. You have to keep track of all constructors and destructors and their progress along the body yourself, and I assume it must be fit for exceptions as well?
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.
I have no doubt that a Rust compiler can be implemented in C. But it's a different project to write one in C from start than trying to migrate an existing C++14 based project to C. The former is likely "easier". An alternative approach could be to migrate the C++14 code back to C++98 and get rid of the exceptions, which makes it transpilable to C (using the cfront approach). Though the result might not be maintainable C, but still C.
EDIT: if you manage to migrate it back to a sufficiently moderate C++11 subset, or even C++98, you could use GCC 4.7.4 to compile it, which itself is written in C.
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.
I got stuck in a loop on 8 "Adding zero to the right", blindly following the tip below the box keeps looping induction introduction. Looping 9 times following the help tip, it eventually complains about an invalid proof state (kernel isn't general enough?). Where's the inductive hypothesis... doh the green box labeled IH on the left side. User error lol. But I feel that folks unfamiliar with proofs would struggle with it.
Also, please remove the rise-in animation so that switching proofs feels faster and less flashy. The rest of the website design has enough flash.
Enough complaints, pretty cool! I did all 20 exercises. Thanks for sharing.
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.
Just thought of how to fix the problem I had. Since the program already highlights the inductive hypothesis blue (but doesn't underline), consider adding a clickable underline to it (Rewrite with IH) instead of requiring the green IH box on the left (banner blindness). See if you can get rid of any drag&drop features and focus more on underline and click (TouchProof, not DragProof). Then the tip box would only need to explain clicking underlined terms.
And another thing, when 2 underlined terms nest (say, Sn+0=0 with underlines on Sn+0 and n), hovering should highlight only the more specific term (hovering on n highlights both Sn+0 and n the same color).
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 :)
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.
I recently got the Anker 140W. I bought a MacBook, and apparently they come without a charger these days. So instead of buying an expensive Mac charger, I figured the widely recommended Anker 140W offers a lot more functionality for less money.
Yep, I gave up on them for now. One of my older laptops also needs a charger that has the third ground pin, lest the trackpad become laggy due to electrical joise. I couldn't find a compact gan charger with a three pin plug and the third actually being connected to ground.
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.
I miss tomsrtbt and all the other single floppy distros, it was surprisingly complete for 1.44MB (including networking, with more protocols than the average browser, and text editors): https://web.archive.org/web/19990506100919/http://www.toms.n... (mulinux iirc boasted about having 100 commands or something like that)
The open paren being part of the tokens was always weird. I could imagine that doing strange things for the parser; when it sees a close paren it needs to know that several of the preceding tokens may have an open paren even without having a '(' token.
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.
Having just recently heard about Ghidra and started using it with Claude. I am absolutely blown away how little resistance it has decompiling old Win95/98 binaries. It's turning into a bit of a hobby of mine to take old software, decompile and find hidden treasures like images or messages.
There's this unfortunate common misconception (that LLMs luckily don't tend to share) that reverse engineering is illegal or immoral, when it's both a great source of learning, a necessity for things like interop/preservation, and even has explicit carve-outs in the copyright laws of many/sane countries.
I know my government has a good amount of reverse engineers on the payroll (mostly in the security services).
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
Typically the approach taken by people who are concerned about legal issues regarding disassemblies is that they distribute a script file that contains all the code/data annotations, comments, variable names, and labels, and then the user can feed this file and a copy of the original binary into the disassembler to reproduce the disassembly. Here's a random example for a 6502 codebase: https://github.com/TakuikaNinja/FDS-disksys . IDA Pro has this functionality built in, you can export a .idc script file that will reproduce the .idb file if you load the original binary into a fresh instance of IDA Pro and then run the script. Maybe Ghidra has something similar, if not I bet you can get your AI to write export/import scripts for Ghidra.
> It's highly likely that the original implementation language was assembly.
Agreed. I did a bit of development on a TI-84+ years ago and I was not a skilled programmer back then so only used TI-BASIC, but the fact you could only write apps in assembly makes me think the operating system was the same. ticalc.org had a gcc fork from memory though I don't recall which calculators it targetted.
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.
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...
reply