Sky is a small language that asks a deceptively interesting question: what happens if you take everything that makes Elm compelling and point it at the server instead of the browser? The project compiles a statically typed, Elm-inspired functional language down to Go, produces a single binary, and frames the result around server-driven UI. Each of those three decisions has real engineering reasoning behind it, and taken together they point at a design space that the broader ecosystem has underexplored.
The Elm Architecture and Why It Travels
Elm’s lasting contribution is not the language itself so much as The Elm Architecture, usually abbreviated TEA. The pattern is simple enough to state in a few lines:
type Msg = Increment | Decrement
update : Msg -> Model -> Model
update msg model =
case msg of
Increment -> { model | count = model.count + 1 }
Decrement -> { model | count = model.count - 1 }
view : Model -> Html Msg
view model =
div []
[ button [ onClick Decrement ] [ text "-" ]
, text (String.fromInt model.count)
, button [ onClick Increment ] [ text "+" ]
]Model holds state. Update is a pure function from (message, old state) to new state. View is a pure function from state to a description of the UI. The runtime loop drives everything: render, wait for user input, call update, render again.
What makes TEA attractive beyond Elm’s native context is that it is essentially a specification for how state flows through a system. Redux, Vuex, and dozens of other state management libraries borrowed from it without requiring Elm itself. The architecture does not care whether the view function produces browser DOM, terminal output, or HTML strings. It is a loop with a clear contract.
Sky takes that portability seriously. Instead of the view function producing virtual DOM for JavaScript to reconcile, it produces HTML that Go serves over HTTP. The loop runs on the server.
Hindley-Milner Without the Browser Wrapper
The type system is the other major piece. Sky uses Hindley-Milner type inference, the algorithm that powers Haskell, OCaml, and Elm itself. HM is worth understanding concretely because it is what separates Sky from a Go preprocessor.
The algorithm works by assigning fresh type variables to all unknowns, generating equality constraints as it walks the AST, and then solving those constraints through unification. A function like:
fn identity x = xgets assigned type α → α automatically. The compiler proves that whatever type you pass in comes back out, and that proof holds for all possible types simultaneously. No annotation required, and the guarantee is backed by the unification algorithm rather than convention.
What this buys you in practice: if your view function expects a User record and you pass it something missing a required field, the error appears at compile time. The compiler does not need you to annotate every variable; it infers the constraint graph from how values are used and rejects programs where any constraint cannot be satisfied. This is the same property that lets Elm claim no runtime exceptions in well-typed code.
The challenge Sky faces is that Go’s type system is substantially less expressive. Algebraic data types, the type Msg = Increment | Decrement pattern above, do not exist natively in Go. Pre-generics Go encoded them as interface{} with type assertions, which is both verbose and unsafe. With Go generics available since Go 1.18 there is more to work with, but encoding a full ML-style sum type still produces generated code that is opaque and difficult to debug directly.
This is the same wall that Oden, an earlier Hindley-Milner-to-Go language from around 2016, eventually ran into. Oskar Wickström archived the project partly because the generated Go was so difficult to introspect that the debugging experience suffered severely. Sky is attempting roughly the same translation; how it navigates that encoding is the most important open question in the design.
Server-Driven UI Is Having a Moment
The server-driven UI framing puts Sky in a growing camp. The core idea is that the server controls what renders rather than sending raw data for the client to assemble. The browser becomes a thin display layer.
HTMX takes this to its logical extreme: the server returns HTML fragments, and the client just swaps them into the DOM based on declarative attributes. No JavaScript framework, no client-side state management, no virtual DOM diffing. A form submission returns an HTML snippet and HTMX patches the page.
Phoenix LiveView takes a different route. A persistent WebSocket connection keeps server and client synchronized. The server holds state in an Elixir process, re-renders the view on each state change, and sends minimal diffs over the socket. The client gets a small JavaScript runtime that applies those patches. The experience is close to a single-page application but all logic lives in Elixir.
React Server Components sit at another point on the spectrum: some components run only on the server and never ship their JavaScript to the browser, while client components hydrate normally. The boundary is explicit and type-checked across the network.
Sky’s position in this space appears closest to LiveView conceptually, minus the WebSocket layer. The TEA loop runs server-side. User interactions trigger HTTP requests. The server runs the update function, produces a new Model, runs view, and returns HTML. If this analysis is correct, Sky gives up LiveView’s partial-update efficiency in exchange for a much simpler infrastructure story: one Go binary, no Elixir cluster required.
The Single Binary Argument
The deployment story is where Sky most clearly differentiates from Elm itself. Elm compiles to JavaScript. Running an Elm application requires a browser or Node runtime, plus whatever backend you build separately to handle persistence and business logic. In practice you are maintaining two codebases in different languages with different build pipelines.
Go’s compilation model is the opposite. go build produces a single statically linked binary with no external dependencies. You copy it to a server and run it. A Docker image can be built FROM scratch, containing nothing but the binary itself. Cross-compilation is built in:
GOOS=linux GOARCH=arm64 go build -o myapp ./cmd/myappFor a full-stack application, the appeal is that Sky’s output is a single artifact. The type checker, the server-side update loop, the HTML rendering, and the HTTP server all compile into one file. The developer writes Elm-style functional code; the deployment team gets a Go binary. That is a meaningful improvement over maintaining both a Node server and an Elm build pipeline.
The tradeoff is that Go binaries embed the Go runtime, so even a minimal binary starts around five to ten megabytes. That is negligible for server deployments but worth noting if you are comparing against a compiled C or Rust binary. Stripping debug symbols with -ldflags="-s -w" helps.
What the Trade-offs Actually Look Like
Sky is making a collection of bets. Hindley-Milner inference catches whole classes of errors before they reach production, but only if the type system is expressive enough to represent your domain. Go’s structural typing and interface model can approximate ML-style types but the approximation leaks. If Sky’s code generator is doing significant work to close that gap, users will eventually encounter type error messages that point at generated Go rather than their Sky source, which is the worst possible debugging experience.
The server-driven UI model eliminates client-side state management complexity, but it trades that for stateful server processes. Every user’s TEA loop state lives somewhere on the backend. Scaling horizontally requires either sticky sessions, external state storage, or redesigning the model to be stateless between requests. LiveView handles this through Elixir’s distributed process model; Go HTTP handlers are stateless by default. How Sky addresses this is a critical architectural question that will determine whether it handles anything beyond simple CRUD applications.
The no-runtime-errors guarantee that Elm provides in the browser depends on the quality of the type checker and the completeness of pattern match coverage. Elm achieves this partly because the language is deliberately constrained, no escape hatches, no null, no type coercion. Sky inherits those constraints in its source language, but the Go backend introduces its own failure modes that Sky’s type system may not be able to express or prevent.
Whether This Matters
Small experimental languages like Sky rarely achieve mainstream adoption, but they almost always contain a useful idea. The idea here is that TEA’s architecture is not browser-specific, and that Go’s deployment simplicity is worth more than the Go language’s type system alone. If Sky’s type checker is solid and the code generator handles the sum type problem gracefully, it could be a pleasant way to build simple Go web services with enforced architectural discipline.
The source repository is the right place to look for current syntax, working examples, and what server-driven UI means in concrete HTTP terms. The project is early. But the design space it occupies, sitting between Elm’s functional discipline and Go’s practical deployment model, is territory worth watching, particularly as the server-driven UI renaissance continues to produce serious alternatives to the JavaScript-heavy client model.