Conversation

Replying to

and

But that is not how we build code. Someone writes an opaque mechanism where "the implementation is the meaning", and someone else builds exactly the same kind of thing on top of that, just a little bit different. So you get layers that a compiler cannot see through.

1

Replying to

and

I don't have a practical solution btw. Even in my own very isolated world where a lot is written from scratch, I run into this issue all the time... Something that has helped me to structure code is to ask "could I in principle write a compiler for the code I'm writing manually".

1

Replying to

and

If there is no "reducer", complexity is always just going to grow, because that is the easiest way to build something to solve a problem. However to build a "reducer" or "evaluator", you need a way to define meaning other than a black box implementation.

1

Alex Weisberger

Replying to

and

I completely agree. This idea of a lang that compiles to a distributed system keeps popping into my head, but it seems like you'd need to build everything from scratch because of the lack of semantics of any target lang / tools. WebAssembly does have a formal semantics though

1

2

Replying to

and

I saw on your profile that you are writing about this.

1

Replying to

and

Have you guys looked at unison or darklang?

1

1

Alex Weisberger

Replying to

and

I'm vaguely familiar but I'll definitely give them a closer look. I saw a talk about Unison where I thought the point of the lang was the content-addressability. And Darklang is self-described as limited to the backend - my dream is a full-stack solution.

1

1

Replying to

and

Ah me too, what I really want is to be able to deploy a service and have that be as simple as writing a phone app.

1

1

Replying to

and

And of course get redundancy/scale automatically as part of that. "The pit of success" but for services.

1

1

Alex Weisberger

Replying to

and

I think it should be easier than writing a mobile app honestly. For example, the redundancy / scale aspect. That's something that an algorithm can figure out better and more consistently than we can. It reminds me of register allocation in a compiler - no one does that by hand.

2

1

Replying to

and

thanks for the links My efforts have mostly been trying to understand by building small things from scratch. I started building a system in Erlang for distributed dataflow, also including generating C for small microcontrollers. Should probably blog something...

4:23 PM · Jan 11, 2022Twitter Web App

Replying to

and

The observation in this context is that the application is often trivial, but the systems programming aspect is really not.

1

Alex Weisberger

Replying to

and

Even "systems" programs can have simpler representations! Take the sel4OS - they wrote a high-level specification of the functionality, then proved that the C code implements it. The high-level spec was much more useful for proving security properties: sel4.systems

1

Alex Weisberger

Replying to

and

I would read 🙃