|
|
|
|
|
|
by aphyr
2181 days ago
|
|
|
There's a lot of research into this, actually! Folks have been working on ways to extract executable code from Alloy, TLA+, Isabelle/HoL, and Coq specifications. That doesn't help with implementations which don't use codegen though--and it doesn't help you with the parts of the program that aren't formalized. |
|
|