perhaps I'm missing the intent, but would it be feasible to have formal verification specifications like with TLA+ act as a blueprint for generating machine code?
It would be fairly cool to be able to design a system using tools like this and have a way to translate it without the possibility of introducing errors during translation to code.
Perhaps what I'm thinking is more automatic generation of test cases? But I'm not quite sure what my brain is trying to watch onto here.
It would be fairly cool to be able to design a system using tools like this and have a way to translate it without the possibility of introducing errors during translation to code.
Perhaps what I'm thinking is more automatic generation of test cases? But I'm not quite sure what my brain is trying to watch onto here.