[HN Gopher] Streams, Calculational Proofs and Dafny
___________________________________________________________________
Streams, Calculational Proofs and Dafny
Author : misonic
Score : 31 points
Date : 2024-08-07 05:55 UTC (17 hours ago)
(HTM) web link (rdivyanshu.github.io)
(TXT) w3m dump (rdivyanshu.github.io)
| User23 wrote:
| Watching Dafny develop has been wonderful. It's taken a lot of
| good ideas from 50 years ago and pushed them into the present in
| modern incarnations.
|
| The predicate transformer semantics (and descendants) approach to
| proving a program has some properties is far more accessible to
| the typical programmer than cracking that egg with the
| sledgehammer of the Calculus of Constructions.
|
| I've been a huge fan of calculational proof styles for over a
| decade now, ever since I did a deep dive into the UT Austin EWD
| archive. Here[1] is his brief explanation, but to really
| appreciate the beauty of the method one has to dig deeper into
| the many practical applications also on that site.
|
| I also recommend looking into Boogie and Z3 for those who are
| curious about how Dafny does what it does.
|
| [1]
| https://www.cs.utexas.edu/~EWD/transcriptions/EWD13xx/EWD130...
| pjmlp wrote:
| Indeed, I thought it would die in MSR, alongside Ironclad,
| instead it took a life of its own.
| two_handfuls wrote:
| Thank you for sharing that document! The style is so
| thoughtful, it's a delight.
| kragen wrote:
| thank you very much for the context!
|
| wrt ewd1300, https://www.cs.utexas.edu/~EWD/ewd13xx/EWD1300.PDF
| is a scan in the original handwriting. it's been a number of
| years since i read it, and i'd forgotten most of its contents,
| though evidently i've incorporated some of them subconsciously.
| and i'm not sure i finished it last time
|
| i've been using [?] and [?] for infix max and min,
| respectively, which is a generalization of their boolean-
| algebra use and appropriate to their use in the theory of
| lattices (the partial-order kind of lattice, of which the usual
| total order is a special case). unfortunately this clashes
| rather badly with the use of [?] in geometric algebra, aka
| clifford algebra ( _e.g._ , https://arxiv.org/pdf/1205.5935) so
| i've been thinking about changing. dijkstra's choice of | for
| max (supremum) and | for min (infimum) are tempting
|
| a second unfortunate collision is that recent versions of apl
| use [?] and [?] for infix lcm and gcd, which is _also_ a
| generalization of their boolean-algebra use and appropriate to
| their use in the theory of lattices; it 's just using a
| different partial order
|
| i think dijkstra's choice of ';' for relational composition is
| rather unfortunate, though it's probably a better choice than
| my choice of simple juxtaposition in binate
| (http://canonical.org/~kragen/binary-relations) which uses ';'
| for the relational product, which i think is an equally
| unfortunate choice. * is the conventional operator for
| relational composition, and it doesn't introduce such fatal
| ambiguities when typeset, but it poses human-interface problems
| with a normal keyboard (how do you know how to type it?) and
| may be confused with some other kind of infix dot operator when
| handwritten, such as the infix function-application operator
| dijkstra explains here
|
| a reasonable alternative is the [?] conventionally used for
| functional composition, which is the same thing as relational
| composition when the relations in question happen to be
| functions, and so generally introduces no semantic ambiguity,
| as well as less typographical ambiguity in handwriting. it has
| the same human-interface problem as *
|
| with respect to quantification, in
| http://canonical.org/~kragen/sw/dev3/paperalgo i've taken the
| approach ka-ping yee introduced in python, of treating
| quantified operators like S, P, [?], [?], etc., as ordinary
| functions whose argument is a set or sequence; then we can
| notate the sequence with the moral equivalent of a list-
| comprehension. (the notation i use for such comprehensions in
| paperalgo unfortunately will not fit in this margin, but the
| web page displays it well.) dijkstra's choice here of < _i_ :
| _i_ < 10: _i_ 2> privileges dummy variables ranging over
| consecutive integers, but as he implicitly points out, you can
| use any logical proposition, such as < _i_ : _i_ [?] _S_ : _i_
| 2> , and while my choice privileges iterations over concrete
| sequences, you can similarly iterate over any set
|
| i'm more interested in expressing algorithms, while dijkstra
| was more interested in proving properties of algorithms, and
| some of our differences in notational choices reflect this,
| such as this last one
| giraffe_lady wrote:
| Dafny seems really interesting in its own right but every time I
| come across it I just want the story of its... logo? crest?
| mascot? https://dafny.org/images/dafny-logo.jpg
___________________________________________________________________
(page generated 2024-08-07 23:01 UTC)