Andreas Rossberg

There is of course a reason why practically no type checker does this: for this to make sense, you'll need a type system that can essentially represent the full domain...

Just to be clear, mechanisation consists of at least two parts: translating definitions and doing proofs. SpecTec should automate the first, but generally cannot do the second, which still requires...

Very nice, thank you for the pointer! I'm looking forward to seeing these integrated into the archive (although tail calls haven't landed in the standard yet, so we might want...

Nothing prevents a proposal champion from modifying this file in their fork, as long as they undo that in the final merge PR. Hence I'm with @tlively, I don't think...

I agree they should be made available here (especially since the w3c site will probably only have the inferior single-page HTML version). We have talked about this in the past,...

I'm not actually convinced this is a good idea. Depending on the proposal, separating out new tests can be rather unnatural and tedious and create unnecessary work later to properly...

> In cases other than for globals the test cases should be additive, no existing tests should need to be modified. Not sure how you come to this conclusion. Any...

Allowing an implicit coercion from Number to mutable Global does not seem desirable. I think the occurrence of |globaltype| in the second line of the snippet is just a typo?

This seems fine, as long as there is no expectation that we are getting into any of the Unicode messes surrounding normalisation etc., i.e., for determining id equality, we are...

PS: Also, a reminder that Unicode spoofing has become a real security concern. Allowing completely arbitrary Unicode strings in something as central and sensitive as identifiers is elevating that risk....