Finn Hackett
Finn Hackett
So far, PGo has been developed blissfully ignorant of TLA+ 2, and it had not caused problems. When discussing how to implement the sum of a set of integers, however,...
Currently, PGo will crash with `NotImplementedError` if a TLA+ module it's compiling references external definitions. Anything involving `EXTENDS`, `INSTANCE` and a module that is not built-in will cause this problem....
Related to #122, this is an idea about how to verify that PGo-generated code actually does what the model says it does. Key idea: encoded into an MPCal model, there...
Compiler validation: provide an option for PGo to attempt compiling invariants into generated code
It would be much easier to argue PGo's soundness, if generated programs could check themselves. This issue suggests adding a flag to PGo, such that it attempts to extract safety...
TLA+ has a really rare scoping rule where including the _exact_ same operator more than once is ok and does nothing. We currently would flag this as an error even...
Here are some notes on invariants from TLA+ that might be useful when compiling to Go. - "functions" can never grow or shrink their domain. This means that records will...
Numbers in TLA+ are a bit messy. This is a proposal/notes on the minimum numerically correct compilation of TLA+ numbers. Numbers in TLA+ have 3 types, defined in 3 standard...
I found this oddity while trying to figure out a type error in my code by annotating types I thought I knew. Here is a minimal example: ```koka fun test-fun(init:...
I can't seem to pass a generic-typed `var` to a function without nonsensical effects getting added. This seems specifically tied to a bad interaction between typing and `var`, as I...
This request is paraphrased from this issue on Dotty proper, which started as an improvement I was planning on implementing for inliner internals: https://github.com/lampepfl/dotty/issues/8294#issuecomment-585328641. Now it seems we need a...