Hacker News Reader

Comment by skybrian | Hacker News Reader

This quite cool but for an HTTP server, most requests should complete within a few seconds and the average should be in milliseconds. Proving that requests are handled in finite time is useful (some kinds of bugs are eliminated) but it's not really the performance guarantee that's needed in this domain. We will probably be using performance testing rather than proofs for a long time.

View on HN

The "finite time" requirement isn't actually related to performance, it's needed to make sure we can prove meaningful things about the return value. If a function never returns a value (or it "returns after an infinite amount of time") then anything we say about its return value will be a counterfactual, and open to all kinds of paradoxes and inconsistencies.

If we want to enforce some actual performance metric, we can use something like cost semantics ( http://lambda-the-ultimate.org/node/5021 ) to enforce complexity bounds (eg. the "big-O" behaviour), then use a few small-scale tests to relate the constant factors in the model to real world values.

There's no reason a proof has to take any time - propositions as types is a tool to guide us to correct information flow, it doesn't mean we literally run the proof at every step. If we trust the core, we can erase the proof checking at the point of compilation and we're left with identical machine code that has been proven to do exactly what we expect and specify.

I think he was referring to the fact that the request completes in finite time isn't a tight enough bound.

Reply on news.ycombinator.com