IIRC this book unfortunately only proves correctness directly and not runtime. Its runtime proofs are based off an abstraction of the algorithm suitable for direct manipulation by proofs rather than the actual implementation in code.

Does anybody know of any languages that let you prove properties about the runtime of a function directly implemented in the language?

▲

auggierose an hour ago | parent | next [-]

> Its runtime proofs are based off an abstraction of the algorithm suitable for direct manipulation by proofs rather than the actual implementation in code.

What is the difference? You are aware that the code is also only an abstraction, right?

	▲	zelphirkalt 6 minutes ago \| parent [-]
		The difference is, that proving something about an abstraction doesn't prove, that you made no mistakes when translating that abstraction into the actual code running, and therefore you have not proven anything of value about the actually running code.

▲

yuppiemephisto 3 hours ago | parent | prev [-]

https://markushimmel.de/blog/my-first-verified-imperative-pr...

Lean

	▲	saithound 3 hours ago \| parent [-]
		Verification of "runtimes" in the sense of GP is not mentioned at all in the article you linked.