This is very nice! It seems to me it shouldn’t be too hard to accompany at least some refactor rules (such as this one) with a short proof of correctness, maybe under some high level assumptions.
@sorawee do you think that would be feasible, or am I overlooking some difficulty?
You mean like, an informal proof written down in comments? Or using some sort of formal theorem prover?
The more formal the merrier, but an informal proof would certainly be a great start
For example, if one expands into the other, or they both (at some point) expand into the same thing, then you’re done
Does anyone know how to track down or resolve a Redex pict font issue? I use GH actions (so Ubuntu) to build a scribble document that has Redex rendered picts which use unicode characters like 𝑨. But whatever font redex is using doesn’t seem to render correctly and I get a mystery unicode box instead.
I think one thing to try is to see if (text "UNICODE") or so can work for this text function https://docs.racket-lang.org/pict/Basic_Pict_Constructors.html?q=text#%28def._%28%28lib._pict%2Fmain..rkt%29._text%29%29 then the “style” argument in Redex can be configured using the metafunction-style parameters (ant other *-style parameters)
Are you using a rewriter here, or the judgment itself has that unicode name?
no rewriter (in this case); the relation is named 𝑨. So the complete code here is just @(define-judgment-form A
#:mode (𝑨 I O)
#:contract (𝑨 e i)
[----------
(𝑨 (Int i) i)])
@(centered (render-judgment-form 𝑨))
I appreciate the suggestions, but I guess what I am really looking for is some idea on how to fix the problem at the level of the font on this system. I’d rather not change the code.
From what I tried here, the default font of metafunction-style is 'swiss, which maps to Helvetica by default. This is as far as I find get to.
Sorry I that wasn’t able to offer more help.
thank you!
As a side note you can set the Redex font style parameters to a comma-separated string of font names and it will use it as a fallback in case earlier ones don’t define a character (just like CSS’s font-family).
windows 10 on racket 8.0 cs snapshot from yesterday
ok, it turned out to be pretty tricky to find a font that worked for this, but I was eventually able to install the fonts-stix package and set the metafunction-style to "STIX Two Math" and things work. Phew.
I’ve noticed that rename-contract doesn’t work on all contracts. For example, (rename-contract boolean? 'foo) appears to do nothing, as the contract prints as boolean? Could someone please clarify this behavior?
I wouldn’t be surprised if that’s just a bug
That’s interesting: only boolean? is unaffected by rename-contract.
Does procedure-rename work? Also, is this on Racket CS or on BC?
Ethereum uses a lower-level encoding called Recursive Length Prefix, or RLP. When a transaction is signed, for example, the bytes signed are the RLP-encoding of the transaction. A nice implementation of the method in ACL2, a theorem prover, has been https://arxiv.org/pdf/2009.13769\|done. I ported it to Racket for personal use: https://pastebin.com/raw/BJz8yJTt The presentation of the code can be found in this PDF. This is a first draft. My next step is to continue to write a Racket library on top of the JSON-RPC supported by Ethereum nodes.
procedure-rename works on boolean?; I’m using Racket CS
I’ve discovered that rename-contract doesn’t work as expected, for procedure contracts. Namely, the name reverts to the old ->-based name, after the contract has been attached to a value, then retrieved with value-contract.
Is this behavior a bug or intended?
That’s interesting: although the name of the contract returned by value-contract is the old name, the contract still uses the new name in the error message of a contract violation.