_thejanus_

7 ms·

1. 1.▲
   by _thejanus_ 14d ago

   What is this lol. A test where your consumer is orders of magnitude slower than your produce, but you focus on button press latency, as though the task isn’t completed dominated by the slow-ass USART print. 20 bytes is like 1.7 ms to print.
2. 2.▲
   by _thejanus_ 2mo ago

   I think so! You can codegen Ocaml directly, which means you have the benefit of lots of nice compiler libs and tools right out of the gate, but the metatheory is also expressive enough that your source language can be pretty wild with your
3. 3.▲
   by _thejanus_ 2mo ago

   What do you mean by this? I don’t want to be annoying and throw “propositions-as-types” at you, but as I understand it, F* is very much already doing this. Its type system is the proof language/metatheory for making propositions, and i
4. 4.▲
   by _thejanus_ 2mo ago

   Yes, I’ve used the EverParse lib, as well as low* extensively! I found a really nice use case, low* makes writing bare metal protocol parsers incredibly easy and compositional at no obvious cost to performance. It’s a real breath of fresh a