_thejanus_

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. They’re also running freeRTOS preemptively even though it doesn’t help here. Just use the cooperative mode. Or better yet, just write one event loop, since all the workloads are extremely bounded. Or even better yet, use a 555 or something, because this workload literally doesn’t even need a processor. I don’t even dislike embassy or freeRTOS, but this comparison reaches depths of stupidity I thought were impossible to reach without switching to some sort of hypoxic trimix.

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 denotational semantics. Grain of salt though, because I haven’t tried this concept in anger at all

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 its programs are their proofs, and there’s an intermediate form, core F*, that we elaborate to, a partial evaluation phase where we actually use the dependent types to simplify our AST, then codegen/lowering. In your analogy, I would call their core IR the bridge I guess? To clarify, I’m not trying to be a dick, I’m trying to sus out if I’ve understood you correctly

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 air compared to writing one giant horrible whole loop, but it basically optimises down to the same assembly.