One of the aims of pavlov is to give developers and LLMs a model-check-driven development workflow that is superior to both traditional TDD and REPL-driven development. When using pavlov, you should be able to use a model to guarantee that your application does nothing you do not want it to do, and everything you do want it to do.

This is straightforward to do with an application that runs on a single system. Model checking comes for free with the behavioral programming paradigm.

Web applications pose a problem: there are two programs running; each has its own state, and each communicates with the other. Fortunately, the behavioral programming model adapts quite well to distributed systems. For the academic details, see Behavioral programming, decentralized control, and multiple time scales. Here, I will be quite practical.

Here’s what I want:

  • No lock-in to any particular html library.
  • Minimal architectural constraints.
  • First class model checking.
  • Navigate program execution paths with nav in portal.
  • Pick your own transport (request/response, SSE, websockets).
  • No react; no production dependencies at all except for pavlov

I do not want to be tied to hiccup (clj), hiccups (cljs), chassis (clj-only), or any other library. So long as html gets produced somewhere (whether on the client or the server), that should be good enough. This concern is partly driven by the fact that there aren’t many good hiccup options that run on both front- and back-end. (Replicant and Michiel Borkent’s html library are the only candidates I really know of.)

More important are the architectural constraints. Although I do think SPAs are rarely a good idea, sometimes it is the case that there is a significant amount of frontend state that needs to be handled. Most of the time, rich client applications are better served by server-driven approaches like htmx or datastar. But you shouldn’t be locked in to one or the other by the framework you choose!

Being able to model check the whole application (including the UI) is, I believe, the most important. (For that to be convincing, you have to try it yourself.)

pavlov-web: a proof of concept

As a proof of concept, I added a pavlov-web module. Let’s take a look at a couple of examples.

Here’s a short preview of it in action:

Let’s start with simple client-side state. Let’s tie the state from an input element to the textContent of another element in the DOM.

Binding textContent

Here’s what the bthread looks like:

(defn- status-text
  [event]
  (case (:type event)
    :browser-only/reset "idle"
    (get-in event [:dom/input :value] "")))

(defn make-hero-form-bthread
  []
  (b/on-any #{:hero-form/input
              :hero-form/reset}
            (fn [event]
              {:request #{{:type :pavlov.web.dom/op
                          :selector "[hero-form-status]"
                          :kind :set
                          :member "textContent"
                          :value (status-text event)}}}))

Is this frontend or backend code? Happily, it can be either. pavlov-web listens on a DOM node (or nodes) to events with an HTML attribute such as pavlov-on-input=":hero-form". When it sees a pavlov attribute, it sends it to a pavlov bprogram. Where? On the frontend, the backend, or both. That part is up to you. Currently pavlov-web provides helpers to have one bprogram in the browser connected to a server-side bprogram via a websocket.

Because the DOM operations are represented as data, they can originate from the backend as well as the frontend. And they can be tested in the model checker.

In this case, there are two bprograms, one running in the browser, the other on the server. The hero form bthread runs on the client. But you could move it to the server, unchanged, and that would have the same effect.

Dom Operations

Let’s look at some more DOM operations. We saw that we can set the textContent of a DOM node. But what if we had a big table and we wanted to sort it? We could, but it might be slow, or we might lose important state.

For that, we can :request an event that looks like this:

(defn- reorder-grid-dom-op
  [event direction]
  (when-let [child-ids (seq (ordered-row-ids event direction))]
    {:type :pavlov.web.dom/op
     :selector (:pavlov-grid-body-selector event)
     :kind :reorder-children
     :child-ids child-ids}))

Here’s what it looks like:

The Future

pavlov-web is currently experimental. But it does show, I hope, that there are genuinely unique and simpler approaches to web development that have yet to hit the mainstream.