# Week of the 07/01/2024 - #27

**Contents**

*tech*

- Understanding Apple DOS 3.3 boot sequence”
- Random links: moviecart for the Atari 2600 and scrcpy

*science*

- BB(5) verified

# Understanding Apple DOS 3.3 boot sequence”

My Arduino disk almost works. I’m able to read several sectors from the DOS disk, it changes to a couple of tracks and seems to be doing a good job but eventually something goes amiss and the boot breaks. I am able to see the memory contents and compare it to the source code of DOS and I can see much of it in memory. I’m tracking the phase signals and see that we are moving among tracks but something breaks it. To be able to understand at what point of the boot process it’s failing I need to understand how DOS 3.3 boots. Forunately there is good documentation for this. Here are the links I’m using:

- Apple DOS 3.3 source code - This is amazing. This is the source of DOS commented. It show each sector and what is in it and also how it’s loaded into memory. With this I can know what code should be in which address of memory. Comparing here I see what code has been loaded. Github repo
- Beneth Apple Dos - This book describes all the inner workings of DOS.
- A couple of interesting repos to look at - This guy has several Apple 2 related repos that are interesting.

# BB(5) verified

A problem which I’ve mentioned several times here is the famous “Busy Beaver” problem. What’s called `BB(5)`

is basically the largest number of steps a `5`

state Turing machine can execute before stopping, starting from a blank tape. Up until recently, the maximun number of steps was 47,176,870 but it was not **proven** that that was the longest. This month it was finally proved that that program is the longest you can make with 5 states. There is an extensive article in Quantamagazine about it: With Fifth Busy Beaver, Researchers Approach Computation’s Limits. From that site I extract a lot of interesting information to read about:

- Formal definition: “The busy beaver function
`BB(n)`

is defined to be the maximum number of moves a halting n-state 2-symbol Turing machine makes before it halts. Although`BB(n)`

is uncomputable for general n, it has long been conjectured that`BB(5) = 47,176,870`

, and large amounts of effort have been spent trying to rule out any halting machines that might make more than 47.176,870 moves before terminating.” - The Busy Beaver Challenge - This site helps with the verification of the BB(5) problem. From the Quantamagazine article: “The spiritual sequel to the Dortmund hunt began two years ago, when a graduate student named Tristan Stérin launched a website announcing the Busy Beaver Challenge. This time, the participants would cooperate, and everyone was welcome. Over time, the online community grew to include more than 20 contributors from around the world, most of them without traditional academic credentials.”
- Anouncement of the success of proving the BB(5) conjecture - “We are extremely happy to announce that, after two years of intense collaboration, the goal of the Busy Beaver Challenge 922 has been reached: the conjecture “BB(5) 272 = 47,176,870” is proved. Exceeding our expectations, the proof 669 has been formally written in Coq by collaborator mxdys whose work improves on and/or uses the contributions of more than 10 other bbchallenge contributors (see credits).”
- A nice simple description of BB(5) - This article explains what is the BB(5) problem, gives simple examples of Turing machines and shows the BB(5) champion TM.
- Coq proof of BB5 (and BB4) - This is the Github repository with the Coq proof of
`BB(5)`

. It also has the proof that`BB(4) = 107`

. - Hardness of busy beaver value BB(15) - A paper that constructs and explicit 15 state TM which solves Erdös conjecture.
- The Busy Beaver Frontier - “ In this survey, I offer a personal view of the BB function 58 years after its introduction, emphasizing lesser-known insights, recent progress, and especially favorite open problems.”
- Intertings blog - Need to look at this.

## Tools

- Turing machine simulator - This interactive page allows you to load and simulate a Turing machine (TM). Github repo.
- The Coq Proof Assistant - The proof of the
`BB(5)`

conjecture is given in Coq. From the Coq site: “Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, the Verified Software Toolchain for verification of C programs, or the Iris framework for concurrent separation logic), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem, or homotopy type theory), and teaching.” - Github repository - The Coq reference manual v8.19.2 - This is the reference manual of Coq. Coq is an interactive theorem prover. It lets you formalize mathematical concepts and then helps you interactively generate machine-checked proofs of theorems.
- Formalizing 100 theorems in Coq - “This is an appendix to Freek Wiedijk’s webpage webpage on the “top 100” mathematical theorems, to keep track of the statements of the 79 theorems that are formalised in Coq.”
- Isabelle - another proof assitant - “Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. Isabelle was originally developed at the University of Cambridge and Technische Universität München, but now includes numerous contributions from institutions and individuals worldwide. See the Isabelle overview for a brief introduction.”
- A proof in isabelle that “Square roots of primes are irrational” - A sample proof in Isabelle. In it, it is proved that the square roots of primes are irrational. In particular that
`sqrt(2)`

is irrational. - Collection of simulators and tools in python / c++ - Collection of Busy Beaver search tools developed by Shawn and Terry Ligocki.

# Random links: moviecart for the Atari 2600 and scrcpy

Two fun projects I found about:

- Moviecart - Software and Hardware to create full length color movie + audio cartridges for stock Atari 2600
- Scrcpy - Open source Android screen sharing application. From the site: “This application mirrors Android devices (video and audio) connected via USB or over TCP/IP, and allows to control the device with the keyboard and the mouse of the computer. It does not require any root access. It works on Linux, Windows and macOS.”