Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.
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?
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.
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.
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?
Would it be something you could specify in types like a specification or would your system be more interested in analysis?
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.