aweinstock

I do think adding a Noita-style cellular automaton would be fairly straightforward.

Currently Veloren has water and lava, but neither will flow (e.g. if water blocks are manually placed on top of a hill, they won't flow downhill, fortunately this is rare due to worldgen). A simple way to fix this would be to have an ECS system that uses CA-style rules (e.g. a water block with an adjacent-and-below air block swaps places with that air block), though naively doing this would be expensive (iterating over all loaded terrain chunks every tick). A possible optimization would be to detect such blocks, remove them from the main terrain grid, put them in a separate entity-with-terrain-collider (the same kind we use for airships), and only iterate the (sparsely populated) AABB of fluids-that-have-recently-moved. This is similar to what Noita does with keeping track of recently-updated terrain rectangles. Once this is in place, it can be straightforwardly extended with more fluid interactions (e.g. Minecraft-style water + lava = obsidian, more Noita-inspired gases rising).

Section 5.13 advises building a custom type-and-mode checkers (per project, seemingly).

Section 4.1 defines a specific type-and-mode system in enough detail that it seems machine-checkable (potentially with the declarations as-is, with suitable declarations of unary `+` and `-` via `op/3` for modes).

It feels like an omission that the paper doesn't recommend or even mention the existence of an implementation-agnostic, project-agnostic type-and-mode checker.

Has one been developed since the paper was published, or is this not as useful as it would seem/not done for some other reason?

It's probably worth noting that the majority of the development on that library was done on April 1st 2019.

Agda and Idris are the same sort of tool (total dependently typed languages/proof assistants/interactive theorem provers) as Lean and Coq.

For a concrete example of how z3 differs from Coq, consider trying to prove that "for all integers x, there exists an integer y greater than x such that x divides y" (a subgoal of Euclid's theorem on there being infinitely many primes).

Here's a transcript of using the z3 python bindings to ask for a proof:

    $ python
    >>> import z3
    >>> x, y = z3.Ints('x y')
    >>> s = z3.Solver()
    >>> s.add(z3.Not(z3.ForAll([x], z3.Exists([y], z3.And(y >= x, y % x == 0)))))
    >>> s.check()
    unknown

z3 returns unknown (if it had returned "unsat", it would have been possible to extract a resolution-refutation proof), and there's not much that can be done with the unknown.

Here's a Coq interactive session that proves most of the cases (with one subproof left unsolved, it was taking me too long relative to the rest of the proof).

    $ coqtop
    Require Import NArith.
    Require Import Omega.

    Lemma x_le_fact : forall x, x <= fact x.
    induction x;.
    - simpl; omega.
    - simpl; admit. (* Proving `x <= fact x -> S x <= fact x + x * fact x` left unsolved here *)
    Admitted.

    Goal forall (x : nat), exists (y : nat), y >= x /\ Nat.modulo y x = 0.
    intros x; exists (fact x).
    split.
    - unfold ">=". apply x_le_fact.
    - induction x.
        + simpl; reflexivity.
        +
      (* goal here is `fact (S x) mod S x = 0` *)
      unfold fact; fold fact.
      (* goal here is `(S x * fact x) mod S x = 0` *)
      rewrite (Nat.mul_comm (S x) (fact x)).
      (* goal here is `(fact x * S x) mod S x = 0` *)
      apply (Nat.mod_mul (fact x) (S x)).
      discriminate.
    Qed.

Unlike z3, you need to manually tell Coq what the steps are, but it gives you feedback on which steps are correct, and what assumptions are available and what subgoals still remain at each step (I've included some of those as comments, running the proof through the interpreter shows more detail).