[m-rev.] for post-commit review: chapter 3 start to end of 3.4

[Mark Brown]

Hi Zoltan,

Thanks for this. I'll go through the XXXs later today, but a few
comments on the later sections first:
- I wrote the definitions in section 3.8.4 before knowing what
definitions I would need, so I've gone back and forth a bit and it
hasn't reached a fixpoint. It might not need to focus on closed
formulas so much.
- I think I forgot to mention that partial correctness means the
intended interpretation is a model. Also, with the running example I'm
planning on pointing out that our intended interpretation is *not* a
model because of equality. We can point to user-defined equality as
one solution. (I can fix this one myself when I get to it, unless you
want to.)
- Currently I'm writing about committed choice, with a view to giving
the semantics for catching exceptions and user-defined equality.

One thing I've been thinking is that the FOPC chapter could be split
in two, with the first giving the syntax and semantics of the
calculus, and the second showing how programs map to axioms. The first
part could then include a natural deduction system, which we could
later use to prove ad-hoc properties of programs (e.g., that the
completion rules make sense). So it's a bit of work and not a priority
right now, but the question is, is it going too far?

Cheers,
Mark

On Sat, Apr 1, 2023 at 4:04 AM Zoltan Somogyi <zoltan.somogyi at runbox.com> wrote:
>
> For review by Mark.
>
> Zoltan._______________________________________________
> reviews mailing list
> reviews at lists.mercurylang.org
> https://lists.mercurylang.org/listinfo/reviews