The Case for Formal Verification (2013)

Re:The Case for Formal Verification (2013) by userbinator on Sunday April 20, 2014 @08:23PM (#7619023)

I think one of the biggest barriers to formal verification is that it is, for lack of a better term, "too formal". There's a bunch of other terminology, language, etc. you have to learn, and the learning curve is steep. For someone who just wants to prove a few pre/post-conditions on some functions (that's why I looked into Coq originally - and gave up because it was too hard), it's too much. There is a feeling that it is too theoretical. I eventually found it easier to prove what I needed to, manually.

[ Parent | on HN ]

Re:The Case for Formal Verification (2013) by jnbiche on Sunday April 20, 2014 @08:34PM (#7619060)

Bingo, unfortunately. I've been able to learn functional programming in Haskell and OCaml without any formal academic background, but looking at Coq, Agda, Idris, and F*, I despair of learning them without more accessible tutorials or a PhD in computer science concentrating on type theory.

My first intro to Haskell was through "Learn you a Haskell". I think without that type of introduction, I never would have progressed past basic pattern matching and folds/maps/filters. I need something similar for dependent typing.

[ Parent | on HN ]

Re:The Case for Formal Verification (2013) by gsnedders on Sunday April 20, 2014 @10:28PM (#7619444)

There's Learn You An Agda at <https://github.com/liamoc/learn-you-an-agda>, though it never got that far. (I've done comparatively little with theorem provers (v. model checkers), so I can't point you anywhere that useful!)

[ Parent | on HN ]

Re:The Case for Formal Verification (2013) by solomatov on Sunday April 20, 2014 @10:42PM (#7619484)

All these tutorials won't teach you how to use coq or agda. The main problem is that in order to use coq or agda, you need to learn Martin-Lof type theory (or calculus of inductive constructions, which is a similar formalism to MLTT) first, and learn to write code later. Otherwise everything will seem like a magic. There are however, good books on the topic:

* Type Theory and Functional Programming (http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/)

* Programming in Martin-Lof type theory (http://www.cse.chalmers.se/research/group/logic/book/)

[ Parent | on HN ]

Re:The Case for Formal Verification (2013) by mateja on Monday April 21, 2014 @07:23AM (#7620605)

There's a really wonderful tutorial on Coq [1] that holds your hand through all the theory you need to learn. I took a class that used this tutorial and I found it to be very understandable and practical, with hardly any background on formal methods myself. Yes, it's a steep learning curve, but at least with this tutorial, you know the curve you need to follow.

[1] Software Foundations http://www.cis.upenn.edu/~bcpierce/sf/

Hint: Check out the overview [2] to see the chapter dependencies and decide which chapters you may want to skip.

[2] http://www.cis.upenn.edu/~bcpierce/sf/deps.html

[ Parent | on HN ]

Re:The Case for Formal Verification (2013) by EzraVinh on Monday April 21, 2014 @02:04AM (#7620002)

But Haskell is also based on some type system, and yet Learn You a Haskell teaches Haskell without formally teaching this type system.

I've been learning Idris and reading the HoTT book at the same time. I'm not sure what it would have been like learning Idris without any formal type theory, but I believe it would be possible.

[ Parent | on HN ]

Re:The Case for Formal Verification (2013) by solomatov on Monday April 21, 2014 @02:30AM (#7620051)

The difference here is that type system in case of agda and coq is the core of the language, it's very similar to what operational semantics does with usual programming languages. The type systems is a logic via Curry-Howard correspondence, with which program correctness is proved. In case of Haskell it's just a software engineering tool which helps you find errors in your program in a semi-automatic way.

[ Parent | on HN ]

Re:The Case for Formal Verification (2013) by EzraVinh on Monday April 21, 2014 @11:22AM (#7621479)

I would say its a sliding scale, I don't think there is a sharp qualitative difference between Idris and Haskell. Haskell programs can also be thought of as proofs, namely proofs that the variables/functions you define have the types you claim they have.

You mention Agda and Coq. Maybe one difference in our viewpoint is that Idris really is designed for general purpose programming. E.g. you can write a program with almost identical structure to a Haskell program.

[ Parent | on HN ]

Re:The Case for Formal Verification (2013) by solomatov on Monday April 21, 2014 @12:30PM (#7621899)

>I don't think there is a sharp qualitative difference between Idris and Haskell.

Yes, there's no such a difference. However, in order to use Idris to its full potential, you need to use dependent types. It's just like writing procedural programs in object-oriented or functional language. It's possible, however, it's not a very bright idea.

[ Parent | on HN ]

Re:The Case for Formal Verification (2013) by dllthomas on Tuesday April 22, 2014 @06:57AM (#7626885)

I've been wondering if you could do something like "gradual typing" with full blown proof (or at least dependent types).

[ Parent | on HN ]