In a previous post I described the high level conceptual design for Votebase, a governable server intended to act as a flexible foundation for a new era of governance experimentation. Read that before this, or you'll be confused.

In this post I'm going to discuss my full long-term technical plan for Votebase, segmented into three named (opens new window) milestones: Bronze, Steel, and Adamantium.

In all these planned releases the same basic ideas will be present:

• Votebase is a server that hosts Rulesets with fullstack capabilities, since they can store data, run server code, and return arbitrary web responses (opens new window).
• Votebase allows Rulesets to enroll and manage members, work with their allowed portion of the database, make HTTP requests, create and manage child Rulesets, create and manage both recurring and one-time Events, and replace the Ruleset with a new Ruleset.
• Votebase must prevent breakage and errors as much as possible:
  • Ruleset functions are necessarily user-submitted code and so must be safely contained
  • Input/output data for Actions and Views must be well-typed
  • Rulesets must not be able to interfere with each other in undeclared ways
  • Actions and Views must not be able to alter their database definition
  • Views must not be able to mutate data
  • When Rulesets are replaced the transition must be consistent and not cause failures

Bronze: usable MVP release

This is what I'm working toward today. The basic building blocks are Postgres (opens new window) for data storage, Rust (opens new window) for all Votebase code, actix web (opens new window) as the server framework, and Rulesets are written in Typescript (opens new window) and run using a custom deno_core (opens new window) Runtime.

Correctness is defended in these ways:

• The deno_core Runtime is a sandbox around user-submitted Typescript.
• All Ruleset Typescript is type-checked using the ambient Typescript Runtime declaration (opens new window).
• Actions and Views define zod (opens new window) schemas for inputs and outputs which are translated to jsonschema (opens new window) and validated at the Rust server level using the jsonschema crate (opens new window).
• Rulesets define a db_migration that is intended to migrate that Ruleset's schema object (opens new window) from its previous version to the new version. Rulesets also provide a "from scratch" db_schema that is the SQL one would run to create the DDL objects as if no existing schema object existed. This db_schema and db_migration are diffed against each other using temporary podman (opens new window) containers to ensure they are consistent.
• The Runtime enforces permissions for Actions and Views using a combination of postgres roles and checks in the Runtime itself.
• Consistency of Rulesets is enforced within the Runtime functions to propose Ruleset replacement Candidates and actually swap a Candidate in. Candidates are checked to ensure the Ruleset tree changes make sense, for example that all References follow the rules and all child Rulesets are recursively consistent.

I've chosen the name "Bronze" for this release because, while useful and worth doing to begin experimenting with actual groups, there are fundamental limits of especially Postgres and Typescript that make it very difficult or even impossible to guarantee the correctness and consistency of all Ruleset code, especially while achieving good performance.

The fundamental limitations of postgres roles and connections mean that pooled connections can't be dynamically swapped to a different role in a truly secure manner, since RESET ROLE (opens new window) can always be executed to regain the permissions of the original connection. If Votebase were to follow the normal practice of having a single connection pool those connections would need to be able to swap to any Ruleset role, meaning any malicious or careless Ruleset function could interfere with any other Ruleset. The choices aren't very good:

• Reconnect to the database for every Action/View execution or Candidate replacement (a performance disaster).
• Maintain connection pools for every Ruleset role (similarly impractical due to postgres connection limits).
• Maintain a single connection pool in the normal way, but use a combination of regex and AST analysis to reject Ruleset Candidates if they contain SQL that could do any form of RESET ROLE or dynamic SQL execution (opens new window) (very high risk from a security perspective). Unfortunately this is the choice that seems most unavoidable.

Further, it's very frustrating for all permissions checks to happen dynamically during Ruleset execution. It's entirely possible for a Ruleset author to create a Ruleset that is simply broken because it will try to perform actions it isn't allowed to. Testing isn't a reliable strategy to prevent these errors.

Even worse is that some things simply cannot be done safely. Postgres doesn't actually enforce function volatility categories (opens new window), so it's impossible for Votebase to allow Rulesets to Reference security-definer functions from one another while maintaining the guarantee that Views never mutate data. Instead References must enumerate permissions to ensure the Reference works properly. Postgres in general is very difficult to use in a manner that is safe, fast, and ergonomic.

I'm on the record that a type-checking error is literally infinitely better than a runtime error, both because a runtime check takes time and so degrades performance, and because a type-checking error can be fixed before the code is actually shipped.

Unfortunately there simply aren't any mature and performant database engines that have meaningfully better static analysis capabilities. Most are actually much worse than Postgres!

In a shared server like Votebase it's especially important for the code to be as robust as possible, since the intention is that Ruleset code can only be changed with some sort of group decision! At this stage I will both advise people to design their Rulesets to be pretty easy to change, and will keep a remnant of the admin model so that either the Votebase organization itself or one of the Members of the Polity can perform and admin Ruleset replacement to fix obvious bugs.

Steel: statically checked postgres

This release would be mostly the same as Bronze, but all the Postgres code and permissions would be checked using a static analyzer (opens new window) instead of with the scary hodge-podge of roles, query linting, schema diffing, and restrictions on security-definer functions.

This would improve the database interaction in every way. All SQL could be checked at the type level before a Ruleset is committed, meaning only a bug in the analyzer could allow a View to mutate data, any function to alter the DDL, or a Candidate migration to fail for non-data reasons.

However we'd still be far away from a truly bulletproof implementation, since the SQL could still encounter surprise errors from inconsistent data, and the Typescript wouldn't have changed at all. The promised land lies in the direction of formal verification (opens new window)...

Adamantium: Rulesets in formally provable languages

For a long time I've wanted to build both a practical and mainstream verifiable language, and a new data language with similar principles. Obviously building entirely new languages is a very large project (LLMs have only made slapping together shallow web apps easy, they haven't changed anything when building deep infrastructural systems (opens new window)), so I won't go into those grand ideas here.

I'll make due by describing the ways Votebase would be much more safe, robust, and therefore easier to build in, if all Ruleset code could be written in formally verifiable languages.

• All permission checking of all kinds would happen at the type level. Roles would only exist as type system constructs.
• Database constraints would be more like liquid types, with that level of arbitrary expressiveness. You could statically know that your entire application from the frontend to the database couldn't possibly violate an invariant.
• Ruleset Candidate checking would be fully equivalent to type checking. All the server would have to do to check a Candidate is type check it as a migration.
• Flow Effects would make it possible to know ahead of time if an error from some necessarily dynamic check was even possible, so all Ruleset code could be written fully defensively and never be surprised by an error.
• Rulesets that could possibly deadlock or hang could be rejected outright rather than relying on the Runtime to kill them.

Formal verification in basically all contexts unlocks huge benefits. For Votebase it would enable a truly transformative degree of safety and robustness, which would be incredibly beneficial since a successful governance server used by millions or even billions of people would be the subject of intense scrutiny and attack. It is just like many other systems in our world: it really needs to be much more safe and secure than it is!

---

So that's the plan, at least as of now. I hope this seems compelling and worthwhile. Let me know if I've missed something!