News for hackers. Stuff that matters.

A comment on The Case for Formal Verification (2013). Parent comment

Re:The Case for Formal Verification (2013) by lmm on Monday April 21, 2014 @04:16AM (#7620250)
> you are inherently limited in terms of what you can prove to whatever it is that the type system can express

Does that actually limit you? E.g. I can imagine using a monad-like structure in Haskell to construct things like "procedure guaranteed to terminate in <k primitive steps".

[ Parent | on HN ]
Re:The Case for Formal Verification (2013) by chriswarbo on Monday April 21, 2014 @09:15AM (#7620876)
Well, considering that the article talks about Coq, which is completely built around a type system (plus a termination checker), it's not that limiting.
[ Parent | on HN ]
Re:The Case for Formal Verification (2013) by wsxcde on Monday April 21, 2014 @09:29AM (#7620920)
It's not just about whether it is possible in theory though. I'm sure it is, but if it's too complicated, it won't see adoption. The point I was making is that expressibility isn't just important in your programming language, it's important for your verification scheme as well.
[ Parent | on HN ]