@User I talk to Satnam and Dom every once in a while. Silver Oak and all the Coq based infrastructure is very attractive to us. We were funding Adam Chlipala’s group at MIT (as is Satnam) to work on their Koika language until the continuing resolution. I know you guys (meaning a group a google) was using Bluespec at one point. Is that gaining any traction?