Hacker News new | ask | show | jobs
by dboreham 953 days ago
Formal methods have been used in CPU design for nearly 40 years [1] but not yet for everything, and the methods tend to not have "round-trip-engineering" properties (e.g. TLA+ is not actually proving validity of the code you will run in production, just your description of its behavior and your idea of exhaustive test cases).

[1] https://www.academia.edu/60937699/The_IMS_T_800_Transputer