5 ms·
How to write correct code by construction using the Coq Proof Assistant
- ftxbro 3y ago[flagged]
- dang 3y agoPlease don't do this here.
- dudus 3y agoI agree with you here 99% of the time. But this one is too on the nose. This might qualify as the 1%.
- hotnfresh 3y agoI’d blame this one on the headline author. You don’t do that by accident.
- dang 3y agoThe article title was obviously a troll (I've changed it to the subtitle now). The HN guidelines ask commenters to abstain not only from feeding trolls but also from gobbling their bait: "Please don't pick the most provocative thing in an article or post to complain about in the thread. Find something interesting to respond to instead." I know it's a lot to ask, but we have to, given the site mandate, and anyway why not? It's an interesting experiment to work on as a community. https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html
- Exuma 3y agoYou have to admit it’s a good one though. Haha. I don’t want this place to become a cesspool like Reddit but once in a blue moon I do need a good laugh
- dang 3y agoNot sure I'd agree it was a "good one" even before this joke was made a million times. Certainly not after.
- dmonitor 3y ago[flagged]
- deleted 3y ago[deleted]
- beachy 3y agoWithout being able to see the flagged comment, I'd venture the authors had a quiet chuckle when titling this piece.
- dang 3y agoI've unkilled it for you.
- deleted 3y ago[deleted]
- andrepd 3y agoFunnily enough, the pun is intentional and the reason that name was chosen.
- dang 3y agoI know; that's one of the components of this endlessly looping cliché.
- agumonkey 3y agoInteresting article, they list applied use of the theory on mainstream tools, things I never see on my readings. https://plv.mpi-sws.org/rustbelt/popl18/ https://plv.mpi-sws.org/rustbelt/popl18/ for instance. Very cool
- nextos 3y agoAlso take a look at Dafny, Why3/WhyML, and Ada/SPARK. Very pragmatic tools that are getting some industry adoption. Coq and Isabelle also see some use, but they are more costly to use in my experience.
- JonChesterfield 3y agoI can't tell if this is pseudocode or what proof in coq usually looks like: Theorem NestedTreeContains1: forall (t: tree), t = Node example 2 (Node Nil 3 Nil) -> contains 1 t = true. Proof. nail. wreck t. - wat. - wreck H into Ht1, Hv and Ht2. sub Hv. evaluate. sub Ht1. just ExampleTreeContains1. Qed. Theorem, forall, qed look fairly likely. Are there built-in operations in coq called 'wat' and 'wreck'?
- Smaug123 3y agoThey are not built-in, no. https://github.com/awalterschulze/ccc-talk/blob/1e781326d2e3c372b6d49bc2f6ff5737dc6757d8/Coq/src/BST/ConstructionToolbox.v#L24 https://github.com/awalterschulze/ccc-talk/blob/1e781326d2e3...
- legobmw99 3y agoI used Coq in one class in school, and I never encountered wat or wreck. It’s possible they’re user- or library-defined tactics. One thing I think is important about Coq is that it really is meant to be interactive. Even after a fair amount of usage I still find it somewhat tricky to just read a proof, especially a nontrivial one. A good IDE will show you a panel that includes all your hypothesis and requirements so far, updating as you run each line
- 082349872349872 3y agoA cursory search reveals they're not builtin, but were written for the talk: https://github.com/awalterschulze/ccc-talk/blob/main/Coq/src/BST/ConstructionToolbox.v https://github.com/awalterschulze/ccc-talk/blob/main/Coq/src... nail ~= intros wat ~= discriminate etc.
- colonwqbang 3y ago"wreck" is actually "destruct", "same" is "reflexivity"... It boggles the mind why the author would make up fanciful new names for the fundamental tactics in this "how to" article.
- atq2119 3y agoThe article shows how interesting properties can be proved (with a nontrivial amount of effort). That's cool, but I wouldn't call it correct by construction.
- MaxBarraclough 3y agoIt's a standard phrase in the formal methods field, [0] emphasising that it's an alternative to the usual approach where we hope that our testing (which can never be complete) is enough to catch all the worrisome bugs. Personally, this article didn't strike me as being very easy to follow, or as being the most compelling demonstration of the value of formal methods. At the risk of going off-topic: if you're not seeing the point, I recommend this example using SPARK, a non-functional language. [1] [0] https://betterprogramming.pub/a-taste-of-coq-and-correct-code-by-construction-111bf74d3b98 https://betterprogramming.pub/a-taste-of-coq-and-correct-cod... [1] https://docs.adacore.com/spark2014-docs/html/ug/en/tutorial.html#proving-spark-programs https://docs.adacore.com/spark2014-docs/html/ug/en/tutorial....
- MaxBarraclough 3y ago10 days too late to edit: the first link should have been https://wiki.c2.com/?CorrectByConstruction https://wiki.c2.com/?CorrectByConstruction
- thaliaarchi 3y agoRight, not all of the techniques shown yield code that’s correct by construction. For example, an argument was indirectly given, and that error was only found after writing a theorem involving it and finding it was impossible to prove. In the section “Correct BST by Construction”, they explain the technique of requiring every constructor of a BST to supply a proof that it maintains the properties of a BST. Any modification to a BST constructs a new BST (since Coq is pure), so any operations on a BST must also supply a proof of their correctness. That is correct by construction.
- mirekrusin 3y agoSoftware Foundations in Coq by Michael Ryan Clarkson [0] is great introduction to this topic. [0] https://www.youtube.com/playlist?list=PLre5AT9JnKShFK9l9HYzkZugkJSsXioFs https://www.youtube.com/playlist?list=PLre5AT9JnKShFK9l9HYzk...
- nuancebydefault 3y agoI find the introduction interesting, it somehow clicked. Devs are like toddlers playing with wooden bricks, who are demanded to scale up this act of building to the level of a grown up's house. In fact it often feels that way. You're either asked to extend or improve existing constructions that feel like sticks and stones bound together with rubber bands. Or one feels excited for being allowed to make up such a construction as a demo, not knowing it will be used as a basis for a production-quality construction. I'm not sure if mathematical proof is the way to go. There's just too much code to cover for this approach to be realistic. Most problems are born on the drawing table. The designs seem right on paper and only in practice, during or after building, they become visable.
- zmgsabst 3y agoTurning a foam architectural model into a house without the required cost investment because the foam model was “so quick to make” feels like a frustratingly accurate description.
- brigadier132 3y agoYep, we build a foundation with plywood and styrofoam and then someone comes and asks you to build a skyscraper on top of it.
- trwaw 3y agoWe build a train and then someone asks to turn it into a skyscraper because skyscrapers are the in thing now. It already looks like one on its side, how hard can it be to turn it right side up?
- smaudet 3y agoWhile I do think proof constructed code could be superior, I am not convinced for two reasons: 1. The problem expressed here has to do with a particular, well understood problem. It is not subject to the whims or constraint needs of the "customer". Proof construction is great when the problem is properly understood, I don't know how well it handles constantly changing requirements. (This encompasses business and interaction constraints too - perhaps you can construct a provable correct UI, but will it be engaging or usable?) 2. Test driven development can guide high quality code construction, arguably at lower construction cost. That is the reason I'd argue this has not taken off in comparison to traditional "test" based design. You can argue it produces lower quality code, and you'd probably be right. But in comparison to construction of complex, rich design, I suspect that it produces faster results at lower cost. The provable solution will win out...eventually. Depends on whether it can make significant marker penetration once it is complete. Nevertheless, yes of course we should be building foundations witb concrete not plywood and Styrofoam, so this is a good development. I do think a proper engineering approach with test based verification can build a "somewhat concrete" foundation, at least.
- staunton 3y agoThere's some software where it's important not to have bugs and know exactly what it does, and some where any attempt to specify what it's supposed to be doing, let alone fixing all the bugs, is a waste of time. (And things in between...) Currently, a lot of instances of the first situation get the treatment befitting the second. This is because it's still too hard to use these tools at scale. However, the trend is certainly towards improving tooling and the cost of doing this will go down a lot. Maybe in a hundred years programming will be replaced by either "formally specify what you want", if you know what you want, (AI fills in implementation of how it does what you want, as well as a proof that it does) or, if you only very roughly know what you want, explain it to the chatbot and answer it's questions.
- deleted 3y ago[deleted]
- seanmcdirmid 3y agoAI probably disrupts programming in the next couple of decades, where they produce not only software but static and dynamic validation artifacts of correctness. It’s sad though, I would have really liked to see how human programming could improve with better tooling, it seems like a lot of formal specification work (and program synthesis using such) could be improvised with just better user interfaces.
- rgmerk 3y agoSo the AI spat out code and a formal spec and a theorem prover spat out a proof that the code is consistent with the formal spec? Great. Does the formal spec represent a complete and accurate description of what the code is supposed to do? shrugs
- seanmcdirmid 3y agoIf an LML can write an essay that humans can read, surely it’s conceivable that it could spit out proofs/tests/docs etc…in a human readable form. So really, you can just decide for yourself then.
- stepchowfun 3y agoIf you're already familiar with a functional programming language like Haskell or OCaml, you have the background to work through my Coq tutorial here: https://github.com/stepchowfun/proofs/tree/main/proofs/Tutorial https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor... My goal with this tutorial was to introduce the core aspects of the language (dependent types, tactics, etc.) from first principles. If you're fascinated by proof assistants like Coq or Lean and want to understand how to use them, this tutorial is written for you. Any feedback is appreciated!
- schoen 3y agoI've done Logical Foundations and part of Programming Language Foundations, and some of the stuff in your tutorial is new to me (especially dependent types). Your tutorial is very interesting, but in comparison to the Software Foundations series you have relatively few exercises and they're all at the end of the chapter. I found it helpful to do exercises as I went along, in many cases testing or exercising my knowledge of a new concept or Coq feature right away. So I would suggest writing more exercises and sprinkling them closer to where some of the material is introduced. Also, some of your exercises in some chapters have a pretty steep ramp-up in difficulty, so again it might be nice to have exercises that gradually build in difficulty. These are probably important considerations when readers are going to be working through this material entirely on their own and it might be their first exposure to Coq. (I think your tutorial says it was previously presented in-person, which has got to be a lot easier, since people can ask questions!) Thanks for writing and sharing this material!
- stepchowfun 3y agoThanks for your feedback!
- schoen 3y agoI'd like to add belatedly that I think it's cool that you introduce the Curry-Howard stuff so early on, basically from the very beginning.
- fortran77 3y agoWhy was the title changed? Isn't HN policy to use the original title unless it's very misleading?
- grzm 3y ago'dang changed it to the subtitle because it was trollish: https://news.ycombinator.com/item?id=37374404 https://news.ycombinator.com/item?id=37374404
- deleted 3y ago[deleted]
- deleted 3y ago[deleted]
- jcarrano 3y agoFor a more practical approach (though limited to C) you can try the Frama-C suite. It works by annotating C code, instead of having to manually rewrite the code in Coq. One thing that the post does not mention is that things get nasty real quick if you use actual machine integers (or number generally) instead of ideal ones in Coq- though that can also be due to my own ignorance as an amateur.
- mdnahas 3y agoIf you’re interested, here is my Coq tutorial. http://michaeldnahas.com/doc/nahas_tutorial.html http://michaeldnahas.com/doc/nahas_tutorial.html It has been mentioned on HN before (multiple times). https://news.ycombinator.com/item?id=21625852 https://news.ycombinator.com/item?id=21625852