Our great sponsors
-
-
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
-
oil
Oils is our upgrade path from bash to a better language and runtime. It's also for Python and JavaScript users who avoid shell!
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
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)