planckforth VS principia

This reminds me a bit of how planck is implemented with planckforth. I can't tell you if there are pitfalls or not, but I can understand how it could be an interesting approach.

Show HN: PlanckForth – Bootstrapping an interpreter from handwritten 1kb binary\ (14 comments)

bootstrap.fs is a thing of beauty

https://github.com/nineties/planckforth/blob/main/bootstrap....

It starts off looking like line noise (the very simple interpreter defined in hex) and gradually turns into the forth we know and love.

Fantastic!

interpreter is designed to be very simple. Every built-in word is single-letter and the interpreter just repeats that reads a character, looks it up from the dictionary and executes it. Also there is no error checking.

This is the actual code for the first interpreter, which is a 136-byte implementation of the interpreter followed by a built-in dictionary of 888 bytes.

https://github.com/nineties/planckforth/blob/main/planck.xxd

The first interpreter and language is so esoteric that, for example, the Hello World looks like this.

    $ ./planck

Seems painful. I like this approach:

https://github.com/nineties/planckforth

You start with a very tiny address or bytecode interpreter, much smaller than 512 bytes. Then you load several levels of bootstrap interpreters into it until you have a fairly featureful Forth. So that occupies ram but not program space on the target computer. You would load the non-initial stuff from a remote computer that didn't have tiny memory constraints.

You can check it out here: https://www.principiarewrite.com/

It's crazy to think that we didn't really know for sure whether 1+1=2 until ~1910, yet it's true. That's when Bernard Russell (best known for Russell's teapot, exposing a logical fallacy in Christianity) and some other dude actually proved it from axioms. They laid out the foundation of 1+1 in a book called Principia Mathematica. They worked so rigorously that it took them 360 pages to even prove something as basic as 1+1=2 using the axiomatic method. If you want to use a modern tool like Coq to verify 1+1=2, then the best way of doing this is to formalize Principia Mathematica in Coq.

There are people trying to make it more readable.

Principia

A work from the early 20th century, mathematics, logic.

I think some expert called Bertrand Russell's and A.N. Whitehead's "Principia Mathematica" initiative a "bizarre" piece of work, when seen from the perspective of a programming language designer.

I can't make a qualified statement about this, as I am neither a mathematician nor a language designer. And I cannot find the exact quote on the internet, sorry. Just saying.

In code? See for yourself :

https://www.principiarewrite.com/

Whitehead and Russell’s Principia rewritten in Coq\ (44 comments)