|
|
|
|
|
|
by cobbal
1891 days ago
|
|
|
The fact that CompCert, seL4, and similar projects exist is proof that a large amount of composition is possible if you have enough time to spend on it. It’s true that you can’t compose arbitrary formalizations, but you can architect your formalizations to be composable. Functional or stateful matters less than the engineering work required. |
|
|