4 ms·
How do you write a spec for correctness? Only the small and unimpressive programs can be checked exhaustively.
by archargelod 1mo ago
How do you write a spec for correctness? Only the small and unimpressive programs can be checked exhaustively.
- thorian1828i03 1mo agoNot true at all! Most of the HTTP APIs, and a good chunk of the webapps, that I've worked on can be defined as a combination of an API spec that carves out valid and invalid behaviors, and a set of behavioral tests for the workflows that the client users care about. Working from a codebase which is generated from a spec document (e.g. OpenAPI or gRPC) and use of tools like https://pkg.go.dev/net/http/httptest https://pkg.go.dev/net/http/httptest and https://bun.com/docs/test/dom https://bun.com/docs/test/dom makes this a pretty achievable goal in practice.
- aw1621107 1mo ago> Only the small and unimpressive programs can be checked exhaustively. Even if you assume that statement is true, there are techniques other than exhaustive checking/model checking. Proof assistants/theorem provers/etc. like Rocq/Isabelle/Lean are quite capable of formally verifying programs without needing to exhaustively explore the search space. I'd question the accuracy of that statement in general as well; model checkers like CBMC/TLA+ are handy for proving properties about interesting systems. The latter, for example, sees use for verifying concurrent/distributed systems, which I think can be reasonably described as more than "small and unimpressive"
- rfgplk 1mo agoYou can formally prove the correctness of even massive programs.