-
-
InfluxDB
InfluxDB – Built for High-Performance Time Series Workloads. InfluxDB 3 OSS is now GA. Transform, enrich, and act on time series data directly in the database. Automate critical tasks and eliminate the need to move data externally. Download now.
-
They've also developed a library that plugs into their actual Rust code to verify it (rather than writing a secondary model in TLA+ or P, it's easier to verify the actual system source code).
See https://github.com/awslabs/shuttle and a whitepaper at https://www.amazon.science/publications/using-lightweight-fo...
Disclaimer: used to work at AWS and had some involvement in this stuff
-
oils
Oils is our upgrade path from bash to a better language and runtime. It's also for Python and JavaScript users who avoid shell!
I watched this a few weeks ago, great talk and exciting tool!
Can you expand on this answer about whether the generated code is run in production or not?
https://youtu.be/5YjsSDDWFDY?t=2200
I would expect that generating USB drivers is just as demanding from a performance perspective as cloud services? You have generally have better and more control over hardware in the latter case?
Do you know if the P-generated code is still used for USB drivers, or if they moved away from that approach and just use the modeling process?
The state machines seem pretty low level, so I don't understand in principle why efficient code couldn't be generated from them?
FWIW I'm using 3 or 4 C/C++ code generators for https://www.oilshell.org, and I've the layer of indirection useful in many ways (although it also can make it harder for people to understand)
