Very nice. The fact that the TCP stack isn't in-kernel isn't all that necessary either. You can perform the same abstraction for an in-kernel stack as for an

Very nice. The fact that the TCP stack isn't in-kernel isn't all that necessary either. You can perform the same abstraction for an in-kernel stack as for an in-application stack, though it can often be harder to disentangle a subsystem that wasn't built from the start with that kind of separation in mind. Unfortunately I can't share them, but I have done exactly this sort of thing in embedded projects at work - compile the same C code (which is coded in a style that tries to minimize if not eliminate undefined and implementation-defined behavior) to run on the host that builds it, under a Haskell test harness that tests behavioral aspects using both unit testing and Quickcheck property testing, with Haskell code simulating external stimuli such as interrupts, low-level behavior of storage subsystems, mcu resets, etc. Testing low-level C code, even code that interacts directly with hardware in unprotected domains, is absolutely possible. And also extremely valuable. The usual caveats about test correctness are even more important, though - there's a much higher burden to ensure that your simulated hardware is both accurate and comprehensive in the behaviors it can simulate.