Embedded Computing Design

Large language models have made remarkable strides over the past few years, to the point that entire aspects of software engineering that once required careful, manual human attention are on the cusp of automation. This evolution is akin to the introduction of the first calculators, the first high-level language compilers, or the first search engines, or perhaps the shift from horses to cars as the primary means of locomotion, albeit at a pace unmatched in history.

Developing formally proven code is challenging. It is also extraordinarily valuable: it produces software with a level of robustness that is otherwise unreachable, and you can have very high confidence that your code will not fail over time. But there is no way around it: it’s hard work.

Leveraging an expressive and formal specification from the start makes it easier to respect requirements, provide automatic verification, and prevent problems or detect them early in development.