At Galois we use Haskell for two things:
- Soft real time (OS device layers, networking), where 1-5 ms response times are plausible. GHC generates fast code, and has plenty of support for tuning the garbage collector and scheduler to get the right timings.
- for true real time systems EDSLs are used to generate code for other languages that provide stronger timing guarantees. E.g. Cryptol, Atom and Copilot.
So be careful to distinguish the EDSL (Copilot or Atom) from the host language (Haskell).
Some examples of critical systems, and in some cases, real-time systems, either written or generated from Haskell, produced by Galois.
EDSLs
- Copilot: A Hard Real-Time Runtime Monitor — a DSL for real-time avionics monitoring
- Equivalence and Safety Checking in Cryptol — a DSL for cryptographic components of critical systems
Systems
- HaLVM — a lightweight microkernel for embedded and mobile applications
- TSE — a cross-domain (security level) network appliance