3 ms·
The author should try some more modern formal methods. Tools like Lean and Rocq can do arbitrary math — the limit is your time and budget, not the tool. These
by Ericson2314 9mo ago
The author should try some more modern formal methods.
Tools like Lean and Rocq can do arbitrary math — the limit is your time and budget, not the tool.
These performance questions can be mathematically defined, so it is possible.
- ted_dunning 9mo agoIndeed. And the SeL4 kernel has latency guarantees based on similar proofs (at considerable cost)