[HN Gopher] How to write correct code by construction using the ...
___________________________________________________________________
How to write correct code by construction using the Coq Proof
Assistant
Author : ingve
Score : 69 points
Date : 2023-09-03 20:10 UTC (2 hours ago)
(HTM) web link (betterprogramming.pub)
(TXT) w3m dump (betterprogramming.pub)
| JonChesterfield wrote:
| I 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 wrote:
| They are not built-in, no.
| https://github.com/awalterschulze/ccc-talk/blob/1e781326d2e3...
| legobmw99 wrote:
| I 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 wrote:
| A cursory search reveals they're not builtin, but were written
| for the talk: https://github.com/awalterschulze/ccc-
| talk/blob/main/Coq/src... nail ~= intros
| wat ~= discriminate etc.
| thaliaarchi wrote:
| The only useful ltac I see in there is compare, which can
| save a lot of tedious rewrites, when needing that frequently.
| colonwqbang wrote:
| "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.
| mirekrusin wrote:
| Software Foundations in Coq by Michael Ryan Clarkson [0] is great
| introduction to this topic.
|
| [0]
| https://www.youtube.com/playlist?list=PLre5AT9JnKShFK9l9HYzk...
| ftxbro wrote:
| [flagged]
| dang wrote:
| Please don't do this here.
| dudus wrote:
| I agree with you here 99% of the time.
|
| But this one is too on the nose. This might qualify as the
| 1%.
| hotnfresh wrote:
| I'd blame this one on the headline author. You don't do
| that by accident.
| dang wrote:
| The 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
| Exuma wrote:
| You 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 wrote:
| Not sure I'd agree it was a "good one" even before this
| joke was made a million times. Certainly not after.
| dmonitor wrote:
| [flagged]
| [deleted]
| abraae wrote:
| Without being able to see the flagged comment, I'd venture
| the authors had a quiet chuckle when titling this piece.
| dang wrote:
| I've unkilled it for you.
| [deleted]
| andrepd wrote:
| Funnily enough, the pun is intentional and the reason that
| name was chosen.
| staunton wrote:
| There'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.
| nuancebydefault wrote:
| I 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.
| brigadier132 wrote:
| Yep, we build a foundation with plywood and styrofoam and then
| someone comes and asks you to build a skyscraper on top of it.
| zmgsabst wrote:
| Turning 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.
| atq2119 wrote:
| The 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 wrote:
| It'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-
| cod...
|
| [1]
| https://docs.adacore.com/spark2014-docs/html/ug/en/tutorial....
| thaliaarchi wrote:
| Right, 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.
| stepchowfun wrote:
| If you're already familiar with a functional programming language
| like Haskell or OCaml, you have the prerequisite knowledge to
| work through my Coq tutorial here:
| 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 they work and how to use them,
| then this tutorial is written for you.
|
| Any feedback is appreciated!
| agumonkey wrote:
| Interesting 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/ for instance. Very cool
___________________________________________________________________
(page generated 2023-09-03 23:00 UTC)