Dominik Stolz

I really like the idea of generator blocks. They seem even more useful than generator functions because they can be used, for instance, in argument position as demonstrated in the...

Another alternative to signals might by pidfds. There already exists a crate which uses them with async-io: [async-pidfd](https://github.com/joshtriplett/async-pidfd)

Improved in https://github.com/qaware/kubepad/commit/37343f8670e4b259cd1b4b2a6986c797f7ae4950 This works because when scaling up, a new Deployment is created for each new instance (e.g. 3->4, 4->5, 5->6). The force option allows new Deployments to cancel...

I started working on this in #32. For now, only compute_if_present is implemented.

Partially implemented by https://github.com/qaware/kubepad/commit/46c530105da1b7c1e6010a8ab2b8422fdce3c8e2 I did not have the chance to test this jet, as all apps in my setup are in `running` state after being deployed.

Some time ago, we experimented with changing the encoding of mutable borrows to not include the final value as a subterm and we came up with the following: ```ocaml module...

The unsound example above would be impossible without extensionality for mutable references, right? Since `*^evil == true` would no longer imply `evil == *bg`.

I think it is. For soundness we have to prevent prophecies from ending up in the current value of mutable references. Prophecies are accessible through the final value operator, as...

Regarding arrays: in theory, we could ignore the length but in practice, we can end up with distinct `inv` symbols for array types with different lengths, so we need to...

Why is this unsound? After all `false /\ inv(arg)` is still false.