Kaspar Lund is very smart and amazingly productive so this sales pitch is disappointing. Amazon's work on formal verification of portions of FreeRTOS, for exam

Kaspar Lund is very smart and amazingly productive so this sales pitch is disappointing. Amazon's work on formal verification of portions of FreeRTOS, for example, is sophisticated and impressive. What Lund misses in his characterization of FreeRTOS as "primitive" is how much refinement goes into simplicity in embedded work. Here's an example: FreeRTOS' over-the-air update (OTA) mechanism has been formally verified. Why would you formally verify your OTA update mechanism? Because getting OTA updates right is one of those simple things that turns out to be hard. Hard problems aren't solved by just adding another layer of abstraction; my expectation is that it will be more difficult to establish a Toit system is performing correctly than a conventional bare-metal or RTOS-based embedded system.