On Sat, Jan 2, 2021 at 4:34 PM Dominik Pantůček < dominik.pantu...@trustica.cz> wrote:
> Hello Racketeers (and Robby especially)! > > On 22. 12. 20 1:30, Robby Findler wrote: > > Is Typed Racket able to prove that your use of unsafe accessors is > > actually safe? > > Short answer: YES. > > One question for a start: And what now? > > That's great! (And I can sympathize about the sarcastic thank you-- getting a machine to verify a proof of something you know to be true is really a lot of work!) As for what now, my hope was that if TR could provide that your uses were good then you could rely on TR to follow up with the actual optimizations. Did you find that to be the case? I see you had to give up on the parallelism for other reasons so I guess there is still a ways to go. I'm not going to recommend that you follow this path further, but I guess that if you did there would be grateful people, perhaps starting with Sam. Robby -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAL3TdOOxQobkq9XPtRynXb8OfWs4r0t5n_LUxxJkfr6-ZzcXVQ%40mail.gmail.com.
