Complexity and security reasoning - Haskell

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Uros Nedic

What is proper way to write proofs and reason about complexity of program (like we reason about correctness and resource usage?

Also, same question for security?

James King

I think it depends on what you mean by complexity. You mention "resource usage," does that mean you are familiar with "Big-O," and asymptotic complexity?

If you can state the problem formally there's a way to write lemmas and proofs.

The same goes for security.

Uros Nedic

My idea was to reason in a way like we reason about correctness with dependent types. To have some language constructs to do it automatically.
p.s. Of course I am familiar with "Big-O" and asymptotic complexity.

James King

I don't think there is a "proper" way as far as I know (which is fairly limited) -- but it sounds like an interesting project. What kind of complexity are you thinking about tackling?

James King

Would it be something you could specify in types like a specification or would your system be more interested in analysis?

Julian KG

These are questions I've thought about too, and did a bit of poking around a while back. There's a lot of stuff on the security side (just look up "dependent types security"), but I've found less stuff for doing complexity analysis. That being said here's something that might tickle your fancy http://gallium.inria.fr/~fpottier/slides/fpottier-2011-01-jfla.pdf.