Forth: The programming language that writes itself

Sometimes you can prove mathematically that two different approaches are equivalent, but differ only in name or some parameter, and that's a unification of sorts, without proliferation of standards.

In case of UIs, this is still an open problem and will be for many years, but I suspect we could do it by defining, in some kind of fuzzy logic for example, what a good UI does look like. Then we could transfer elements from one UI into another.

Or we could just start at the edge. For example, we can unify what a "user input" is, and what a "widget on the screen" is. Formalizing everything would allow us to do such transformations on programs, for example, universal input/output remapping. And then we could continue to unify into more specific logic of what input is being read and how things are drawn on the screen.

Untyped lambda calculus (and its sibling combinatory logic) is just language for expressing logic, nothing more. And it already exists (arguably it's one of the first programming languages, predates Forth and Lisp by at least two decades) and is among the simplest ones we know. I actually became interested in LC so much recently because, believe it or not, expressing things in classical logic is often more complicated than expressing things in LC.

> Don't you mean xA = B ?

No, that equation can be created as a special case from equation TAx = B (where Txy = yx is a transposition combinator).

> Not if you require x to be strict, i.e. it must use its argument.

I am not sure it would generally help but maybe you mean it only in case of equations xA=B (not Ax=B as I suggested). I also think this strictness condition would be too limiting.

In equation Ax=B, we can take A of the form R_n A_1 .. A_n, where R_n reduces Ax to x A_1 .. A_n (R_n rotates x in front of n arguments).

So if x is concrete and takes n arguments, we can think of it as "text" (parenthesised expression) in symbols that are to be interpreted as A_1, .. A_n. Requiring that every possible symbol is used in a language text fragment is a weird condition, which doesn't make much sense to me.

In any case, my definition of typing judgment then allows to put a chosen condition on a text composed from chosen symbols, which is quite powerful and can be used to e.g. determine whether a quoted expression is valid. And arguably it is a very natural definition in the context of ULC. (I read to Mock a Mockingbird 30 years ago - in partial Slovak translation - and most problems there could be formulated as the Ax=B equation for x being a concrete term.)

Flipside: it looks like the most productive programmers are those who work alone and not in a large pool. The core point of the article is that team development is slower and less efficient.

Which means management must make a choice: getting good code relatively fast from a small pool of high-value individuals that it must therefore cherish and treat well...

Or get poor-quality code, slowly, but from a large and redundant group of less skilled developers, who are cheaper and easier to replace.

It is a truth universally acknowledged that from the three characteristics of "good, fast, and cheap", you can pick which two you want.

In this case, maybe the choice is as simple as "good and fast" or "cheap."

If the structure of the business or the market requires management to pick "cheap" (with concomitant but unspoken "bad and slow") then the structure, I submit, is bad.

> Sometimes you can prove mathematically that two different approaches are equivalent, but differ only in name or some parameter, and that's a unification of sorts, without proliferation of standards.

Certainly, but that would already be supposing most of the work to unify at the source level is done, unless an extremely strong normalization is possible.

> Untyped lambda calculus (and its sibling combinatory logic) is just language for expressing logic, nothing more. And it already exists (arguably it's one of the first programming languages, predates Forth and Lisp by at least two decades) and is among the simplest ones we know. I actually became interested in LC so much recently because, believe it or not, expressing things in classical logic is often more complicated than expressing things in LC.

(Personally, I prefer combinators slightly more)

I don't deny the power of LC for some uses, but taking one program, reducing it down to an LC equivalent, and then resurfacing as another program (in a different language, but otherwise equivalent), or some other program transformations you may desire, would certainly be elegant in some sense, but very complex. It's like programming in Brainfuck; the language itself is very simple, and making mechanistic tooling for it is very simple, but I don't think the tooling we could invent in 50 years would be sufficient to make Brainfuck simple to read or write. Moreover, formalizations of, say, "button" are not a problem, but scaling to different screens, devices, use cases, and so on will greatly increase the scope. This OS represents input events this way, this hardware provides that sort of data. I think this is the same problem as to why people, everyday, don't bother to make formal arguments almost all of the time. It's not that a formal argument along the lines of "you didn't take out the trash today, so I have reason to be frustrated with you" can't be formulated or proven, but rather that the level of rigor is generally considered both fatiguing and unnecessary.

Any time someone suggests something that should make things much simpler, I'm skeptical. There are things that have essential complexity too great to be made simple, and then humans maybe have an inherent overhead of accidental complexity, above and beyond the accidental complexity we accidentally add. I'm still interested to see where your efforts lead, but I'm not expecting to see cheap nuclear fusion for another 10 years at least, so.

Yup. I am old enough to have posted cassettes rather than 5.25" floppies, although I was using a Z80-based machine that ran Forth and took 5.25" floppies as late as the early 90s. Wildly specialised bit of kit, and I wish I'd stolen it when I had the chance because it's probably been thrown over the side of an oil rig by now.

The first Forth machine I used was the Jupiter Ace, which was a home computer sold in the UK by a couple of guys who spun their company off from Sinclair. It was a bit too underpowered and a bit too late and a bit too weird to really "land" - everyone either had a ZX Spectrum or a Commodore 64 by then, and schools and rich kids had BBC Micros (I got right into 6502 machine code on the one we had in school when I was about 9, and then got my hands on its predecessor, the Acorn Atom). I also had a couple of Epson HX20s that the company my dad worked for had used as data loggers, which had Forth ROMs fitted. That's how I got right into 6809 programming, and that chip is ludicrously suitable for Forth!

I got Cosmic Conquest working on an Apple II emulator but the support code around getting it working is frankly terrifying. I used a fig-Forth disk, and wrote my own implementations of the graphics words used there, which I guess is what the original author did.

Tracking them down has so far proved impossible, and it's quite likely they are no longer around.