[HN Gopher] Formally Verifying Rust's Opaque Types
___________________________________________________________________
Formally Verifying Rust's Opaque Types
Author : BreakfastB0b
Score : 124 points
Date : 2022-08-01 11:42 UTC (11 hours ago)
(HTM) web link (dylanj.xyz)
(TXT) w3m dump (dylanj.xyz)
| yababa_y wrote:
| I love this walkthrough! It reproduces, in narrative form, the
| experience of interactive theorem proving. Great exploration of a
| niche detail.
| BreakfastB0b wrote:
| Author here. Glad you liked it! I've had a real fear of writing
| since High School and so starting this blog is my attempt to
| work through it.
|
| It's a shame that more engineers don't have the time or
| interest to learn formal verification because it's really
| enjoyable once you get the hang of it. Although it rarely
| directly comes up at work, I think it gives a good framework
| for thinking in strongly types languages with advanced type
| systems like Rust, Typescript, or Haskell.
| vlovich123 wrote:
| Personally it's because I don't enjoy solving the problem
| once in one language and then transcribing it into a totally
| different language and worrying I got the transformation
| correct (+ I still need to write all the same tests). Also,
| afaik proof languages don't have libraries for building up
| more and more proofs, and, even if they did, they're not
| going to come bundled with random runtime dependency X I
| picked to implement it. It doesn't feel like it will be an
| enjoyable experience and there's generally little incentive
| from the buyer's end (ie management aren't typically
| demanding it / hiring for it / giving time in the schedule to
| write proofs).
|
| And as far as it helping with other languages, I feel like
| practical TypeScript understanding doesn't benefit
| particularly from proofs. Rust and Haskell I can't make
| claims about but if that's true those languages will suffer
| (but I don't think it's really needed).
| BreakfastB0b wrote:
| I didn't mean to imply that people should be using Coq or
| another proof assistant in their development workflow. More
| that understanding formal verification aids in thinking
| about typed programs.
|
| However no type system of a Turing complete programming
| language can ever be truly trusted as a proof system
| because looping forever or other non-termination can be
| used to prove any proposition. const
| proveAnything = <A>(): A => proveAnything()
|
| The above function can prove any proposition including 1 ==
| 2, by just recursing forever.
|
| However, take Rust's ownership system for example, it uses
| a type system that corresponds to a kind of logic called a
| sub-structural logic that denies one of the axioms of
| typical classical logic systems, namely, the weakening
| axiom, e.g. a function of the type fn
| <A>(a: A) -> (A, A) { ... }
|
| is not possible to write in Rust, but easily writable in
| most other programming languages. Because of this, Rust is
| able to "prove" that the program is free from data races
| which is pretty cool if you ask me.
| tatref wrote:
| Can't the function just return `(a.clone, a.clone())`?
|
| Maybe you mean something like this? `fn extend_vec(to:
| &mut Vec<i32>, from: &Vec<i32>) { ... }`
|
| This does not compile if you pass the same Vec as to and
| from, because of the `&mut`
| brabel wrote:
| Without a trait bound that demands cloneable items, no.
| themulticaster wrote:
| Before I begin - I hope my comment doesn't come across as
| too confrontational. I don't want to invalidate your
| experience, but I'd like to spread information about formal
| verification techniques that are usable today.
|
| > Personally it's because I don't enjoy solving the problem
| once in one language and then transcribing it into a
| totally different language and worrying I got the
| transformation correct (+ I still need to write all the
| same tests).
|
| Isabelle/HOL [1] allows specifying and proving properties
| about a function/program in Isabelle/HOL and then
| generating output in Haskell, OCaml, Scala and SML.
| Granted, you'd need to learn Isabelle/HOL, but you wouldn't
| need to worry about the transformation process.
|
| > Also, afaik proof languages don't have libraries for
| building up more and more proofs, and, even if they did,
| they're not going to come bundled with random runtime
| dependency X I picked to implement it.
|
| The Archive of Formal Proofs [2] is a collection of
| Isabelle theories (proof modules) that you can easily
| integrate into your own proofs. Some proofs in the AFP are
| about specific properties so they're not that interesting
| as a proof library, but many others include reusable
| specifications that are useful in other proofs.
|
| I'm not quite sure about the runtime dependency aspect you
| mention. In general, proofs about data structures and
| algorithms are interesting, but proofs about glue code or
| I/O interfaces are mostly useless and a waste of time
| (depending on the context). For example, proving your
| sorting algorithm is correct is a good fit for formal
| verification, but proving your network code uses the
| correct flags in a socket creation syscall is hardly
| interesting and provable.
|
| I'm only familiar with Isabelle/HOL, so my comment is
| limited to that environment.
|
| [1] https://isabelle.in.tum.de/overview.html
|
| [2] https://www.isa-afp.org/
| dist1ll wrote:
| > It's a shame that more engineers don't have the time or
| interest to learn formal verification
|
| That's the problem with CS, which is full of beautiful and
| intriguing topics. Graph theory, game theory, formal logic &
| semantics, automata, compiler design, theorem proving, type
| theory, computational social choice, resource allocation,
| coding theory, cryptography, distributed computation, etc..
| BreakfastB0b wrote:
| Absolutely! Every time I think there's a boring area of
| Computer Science when I read more deeply into it, it turns
| out to be amazing. Even something which I hated in
| University like Complexity Analysis turned out to be
| utterly fascinating after I read Scott Aaronson's "Quantum
| Computing Since Democritus". It has such deep and
| interesting connections to ontology, epistemology , and
| physics. So much to learn, so little time. Gotta keep that
| story point velocity up!
| ratmice wrote:
| Nice writeup, been a while since I had used coq, it was nice
| to try and work it out from memory, but be able to refer back
| to your post when I got stuck.
|
| Also threw together a tiny lean proof without tactics,
| figured i would post a link to it to avoid spoilers. https://
| gist.github.com/ratmice/ae54d9b27f7afa8cabb7cc84c425...
|
| couldn't get the link to work in the lean-web-editor though.
| yccs27 wrote:
| As someone who's used to functional programming but not familiar
| with any proof systems, I've sometimes applied Curry-Howard the
| other way and used Haskell as a primitive proof system by writing
| the corresponding function (being careful to avoid infinite
| recursion). GHC's support for "typed holes" makes this pretty
| convenient - just write a part of the function and leave a hole
| (_) for the rest, GHC tells you what type is needed there.
| agluszak wrote:
| The title is a bit misleading: you're not formally verifying
| rust's opaque types - you're simply proving a intuitionistic
| logic proposition using Coq. There's nothing Rust specific in
| that proof.
| BreakfastB0b wrote:
| That's totally fair, it does make it sounds like I'm verifying
| the compiler's implementation of it. However it is proving that
| making such a transformation between the two styles of static
| dispatch is always sound.
|
| What would you have titled the blog instead to be less
| misleading?
| agluszak wrote:
| Introduction to Coq theorem proving using Rust static
| dispatch equivalency example
| howling wrote:
| Personally, I find the title to be slightly misleading as the
| proof is essentially just (un)currying for dependently typed
| function.
| BreakfastB0b wrote:
| I'm not sure I understand the connection to dependent types,
| would you be able to elaborate?
| howling wrote:
| Normal currying describes an isomorphism between functions of
| type (A x B) -> C and functions of type A -> (B -> C). With
| dependent types, we can have an isomorphism between functions
| of type ((a : A) x (b : P(a))) -> Q(a, b) and functions of
| type (a : A) -> ((b : P(a)) -> Q(a, b)). What your article
| proves is a bit less generic with Q doesn't vary accoring to
| a and b; i.e. an isomorphism between ((a : A) x (b : P(a)))
| -> Q and functions of type (a : A) -> ((b : P(a)) -> Q).
| BreakfastB0b wrote:
| Yeah that makes sense, thanks for explaining.
|
| I don't want to make it seem like I'm proving anything
| novel here, the proof I work through is definitely pretty
| basic as far as proofs go. It's written somewhat
| narratively because it reflects a train of thought I went
| through a few days ago when reading about existential types
| in Rust. Seeing the theorem (([?] x. P(x)) - Q) = ([?] x.
| (P(x) - Q)) in the blog post made me want see if I still
| remembered enough Coq to prove it, and then when I was
| sitting down this morning to write something I thought it
| would make a good blog post as it explores some deep cuts
| of what I've been learning in Rust and might make a good
| introduction for people into Coq. I'll definitely take it
| on the chin that I titled the blog too ambitiously however
| and I'll be more modest with my titles in the future.
| ArrayBoundCheck wrote:
| throwaway17_17 wrote:
| Can you explain you explain your comments implied link between
| this blog post and what about Rust makes it not a 'proper
| language'? Also, is it just the hype, community, etc that you
| don't like about Rust or is it something else?
| ArrayBoundCheck wrote:
| Look at my username. I didn't like it since rust called
| themself memory safe and didn't force us to do an array
| bounds check. It's been 10years and they still haven't done
| it
|
| (Also all the hype and fearlessness is obnoxious)
| Ygg2 wrote:
| That's just FUD. Rust inserts bounds check automatically in
| debug mode, if needed. Second, using iterators makes bounds
| checking redundant.
|
| And random access `array[intval]` will always be
| performance crippled if intval is provided by external
| system at runtime.
|
| Even if intval is guaranteed to be between
| 0..<array.length, you need to converted it to that type.
| ArrayBoundCheck wrote:
| Just FUD while spreading FUD? Are you trying to say
| release mode doesn't have runtime checks inserted?
|
| What I want is a check outside of the loop then every
| access inside a loop unchecked and fast. Which isn't what
| rust does. Then it throws your memory away if you did an
| oops and went out of bounds
| pitaj wrote:
| > What I want is a check outside of the loop then every
| access inside a loop unchecked and fast. Which isn't what
| rust does.
|
| That's exactly what iterators allow.
| throwaway17_17 wrote:
| I think the caveat to this is that iterators are a
| fundamentally different programming 'construct' than a
| statement block using an index to access elements of a
| container and then having that index increase with each
| loop.
|
| I tend to treat iterators as a non-factor when discussing
| semantics of a language as I will always default to them
| not being a 'language-level' construct. I am not a fan of
| iterators in any case, but then again, I don't
| particularly like any higher level constructs in my 'run-
| time' code.
| sophacles wrote:
| Your "run-time" code with iterators vs with a hand made
| for loop tends to result in the same set of instructions.
| Often the iterator usage will also enable optimizations
| that make the loop faster.
|
| * https://github.com/mike-barber/rust-zero-cost-
| abstractions
|
| * https://carette.xyz/posts/zero_cost_abstraction/
|
| * https://ruudvanasseldonk.com/2016/11/30/zero-cost-
| abstractio...
| throwaway17_17 wrote:
| Once I got through writing this comment I realized it was
| really long and was not particularly enlightening or
| insightful, but I decided to go ahead and post it. If you
| have any opinions on it I'm always to glad to read what
| other people think about language design/usage and
| surrounding topics:
|
| I don't disagree that the translation may result in
| roughly similar assembly/bytecode instructions in many
| languages, and while TFA is Rust-centric and most of the
| conversation has been too, my issues with iterators are
| not restricted to Rust. Further, my objection to using
| them in my own code is not strictly a performance issue
| (although, I am never in favor of coding and hoping it
| gets optimized).
|
| Inherently, iterators are a more complex concept than a
| loop (or the tail recursive equivalent). Iterators are an
| object in and of themselves that are by design more
| complex than a natural number index, then you still need
| the actual looping construct. I am aware there are
| reasons that iterators are preferred and often
| recommended in some situations. However, the
| determination to use an iterator based construct in your
| code is not a universal declaration of fitness, it is
| only a case-by-case determination weighed against
| whatever other factors matter to the people writing the
| code. I also think this applies to the pushing of
| iterators as an idiomatic construct in a programming
| language, i.e. whether iterators are idiomatic is a
| determination that is made by the language designers when
| weighed against the established goals and priorities of
| the language as a whole.
|
| Regarding the iterator-based code enabling optimizations
| that make the resulting compiled code faster than a basic
| while loop: I will admit that there is a possibility for
| this to occur. However, that is tempered by an educated
| guess that the enabling of those optimizations only occur
| because the compiler writers have explicitly coded in a
| 'hot-path' for iterator constructs into the IR. Also,
| there is the chance that the compiler writers use the
| higher level IRs to memoize data about the loop as a
| whole (based on knowledge of the language's iterator
| construct) and the presence of that data at later stages
| of the compiler allow for optimizations to occur, whereas
| the while loop would not trigger the memoization steps
| and then could not produce the optimizations. Both of
| those circumstances are a result of the language
| designers/compiler writers basing code generation (or IR
| generation) off of the idioms of the language and the
| underlying semantic definitions of the language.
|
| As an aside, I am not certain Rust's compiler treats
| iterators the way I described above, but I would be
| surprised if it was not.
| solar-ice wrote:
| The optimisations for Rust's iterators primarily come
| from the fact that iterators can trivially maintain
| Rust's safety properties (skipping runtime checks in the
| code, without an optimiser even being involved) and
| iterator-like constructs are easier for generic
| optimisation passes in LLVM to reason about.
| Arnavion wrote:
| I'm sure you can understand why "I'm going to ignore this
| part of the language because it damages my argument"
| might be convincing to yourself but not to others.
| throwaway17_17 wrote:
| I'm not sure what argument you see me making. I'm also
| not ignoring anything. And I am most certainly not trying
| to convince anyone of anything. In the comment you are
| responding to I am talking about how I view language
| constructs and their impact on my view of semantics. I
| don't have an argument to make.
|
| The closest thing to an argument I am making is that
| iterators are a different language construct than a basic
| looping construct. If you disagree that's fine, like I
| said, I'm not trying to 'win' anything or convince anyone
| of anything.
|
| Edit to refer to sibling comment -- As I said in a
| sibling comment, the iterator loop construct is syntactic
| sugar and that's why I was saying it is different from
| discussing a more basic looping construct.
| solar-ice wrote:
| Rust has built-in semantic support for iterators; the
| compiler knows about the Iterator and IntoIterator traits
| and has specific syntax (the for expression, also known
| as the "iterator loop expression") to use them. In fact
| there is no direct semantic support for the type of loop
| you are talking about.
| throwaway17_17 wrote:
| Rust does have a for in construct that is implemented in
| terms of iterators. However, Rust certainly has a while
| loop also defined as a part of the language. The
| docs.rust-Lang also defines a loop construct that is only
| exited with a break statement. So there is clearly
| semantic support for a looping construct that just loops
| over code and can contain an incrementing index variable.
|
| I would have to check the intermediate language, but I
| assume the for in construct is implemented, at the
| semantic level as an iterator object inside a while or
| basic loop construct.
|
| Edit -- I just checked and docs.rust-langexplicitly
| states that the for in construct is 'syntactic sugar' for
| the common case of looping over a container that
| implements the iterator trait.
| solar-ice wrote:
| A while loop is not semantic support for incrementing a
| number on each loop. It is semantic support for checking
| a condition on each loop.
|
| You can increment a number yourself, but at that point
| you're doing something where there is significantly
| better language support for just using iterators. You may
| as well claim Rust has semantic support for, idk,
| bubblesort, because you can write bubblesort with it.
| throwaway17_17 wrote:
| As I said in my edit, the Rust docs explicitly call out
| the for..in construct as syntactic sugar over a loop
| which contains an iterator in the body, i.e.
|
| 'or-in-loops, or to be more precise, iterator loops, are
| a simple syntactic sugar over a common practice within
| Rust, which is to loop over anything that implements
| IntoIterator until the iterator returned by .into_iter()
| returns None (or the loop body uses break).' [1]
|
| In fact that same page gives the expanded code on it. It
| directly expands to code using the iterator's .next()
| method on each go through the loop. So, I think since the
| difference between the iterator semantics, as defined and
| describe by the Rust documentation, and using an index
| variable and incrementing that variable on each loop are
| not different enough for your exaggerated claim regarding
| 'semantic support'.
|
| But, I'm not trying to convince you to not use iterators
| or that iterators are not useful in some projects. I
| don't particularly care what other developers decide are
| the correct standards for their projects. My initial
| comment for this sub-thread was just trying to point out
| that I tend to view a language's semantics at the base
| level, where iterators are programmer implemented
| features defined for specific types, and that there is a
| definite difference between using iterators and using a
| loop with an index variable for container access. I don't
| think I was wrong to make that observation, and the Rust
| docs seem to support that difference. That's all I was
| getting at.
|
| [1] - https://doc.rust-lang.org/std/keyword.for.html
| solar-ice wrote:
| Using the iterator's .next() method in a loop - or the
| built-in expression for doing so - avoids maintaining an
| integer counter and indexing. It is simply not
| semantically the same thing, and you cannot approximate
| what iterators get you with your counting loop in safe
| Rust code. The difference in semantics is why one enables
| you to avoid overflow checks and the other does not,
| given the semantics of Rust which don't allow skipping
| those overflow checks in safe code.
|
| At a "base level", every language is exactly equivalent -
| they are all approximations of a turing machine - so I
| really don't get that argument unless you are trying to
| argue that every language is really just C in disguise.
| sophacles wrote:
| Sure it there is: for i in 1..n {
| some_mut_arr[i] = T::default(); } //
| OR mut i = 0; while i < n {
| do_something(some_arr[i]); i += 1; }
| solar-ice wrote:
| 1..n is an iterator. The while loop is torturing the poor
| language - it is using the wrong tools to achieve a goal
| that is much better achieved using the things it does
| have direct semantic support for.
| sophacles wrote:
| I see what you mean by "semantic support" now. Fair
| enough that 1..n is an iterator, however it's not an
| iterator over the array we're manipulating.
|
| As for the while loop "torturing the poor language" -
| that's you injecting some preference. It's perfectly
| valid rust, and there's plenty of situations that look
| close to what I wrote (albeit my example was distilling
| down those cases to the core) and which aren't easily
| achievable without contortion to get everything into an
| iterator.
|
| Don't get me wrong - I really like iterators. Sometimes
| though, iterators add obfuscation, particularly after the
| 5th or 6th chained iterator method.
| tialaramex wrote:
| Rust only really has one loop, it's named loop and it's
| an infinite loop (you break to leave it).
|
| So just as Rust's "for" is syntactic sugar, so is
| "while", it will de-sugar into loop with an exit
| condition break at the start, since that's how while
| works _in Rust_.
|
| But this sort of illustrates how limited your model is,
| you're assuming the way loops worked in some language
| you've more experience with, probably C, is just "how
| loops work" but it's a weird feature of one language
| invented decades before the present, but decades _after_
| the fundamentals. It 's like fixating on how the brakes
| worked on the 1971 Ford Cortina. That's not "how car
| brakes work" it's just how the brakes worked on that
| particular model of car, a brand new BMW i4 and a Model T
| are both equally reasonable examples of "how car brakes
| work".
| throwaway17_17 wrote:
| I was under the impression that unless inside an unsafe
| block, Rust required/automatically-placed bounds checks on
| array accesses. The out there was for situations where the
| compiler could 'prove' that the index was within bounds
| statically. But maybe I was wrong about that.
|
| With such a strong focus on bounds checking, are there any
| 'systems programming' languages that you do find
| acceptable?
| ArrayBoundCheck wrote:
| > automatically-placed bounds checks on array accesses
|
| That's exactly why I get annoyed. How will it be fast if
| it branches on every access
|
| > where the compiler could 'prove'
|
| The compiler doesn't prove shit. It lets the optimizer do
| it. It's extremely easy to fool the optimizer
|
| > there any 'systems programming' languages
|
| The ones that don't make false claims (so not v or rust)
| and don't insert code I don't want
| throwaway17_17 wrote:
| Your objection to saying my saying "the compiler could
| 'prove'" is one of the reasons I put the quotes around
| prove. Also, thanks for answering, I didn't want my
| question to seem like baiting or trying to start a string
| of downvotes, etc. I am honestly interested developer
| stances on languages, for whatever reason those stances
| exist.
| gpm wrote:
| Even in unsafe blocks, rust automatically places bounds
| checks on array accesses. It's just that in unsafe blocks
| you get access to additional more verbose functions, such
| as "array.get_unchecked(idx)" instead of "array[i]", that
| don't perform bounds checks.
|
| Unsafe blocks don't change the semantics of code, they
| just let you write code you couldn't write outside of
| them.
| throwaway17_17 wrote:
| That's interesting, I don't know that I would have
| thought about the behavior of the subscript operator as a
| semantic issue in that way. I guess it is a different
| view point to mine. I, nearly, universally view the
| subscript operator as a function that takes a Nat and
| produces the element of the array/list/etc that is stored
| at that index. So, for me, the placing of bounds checks
| when using that function is an implementation detail and
| therefore, if unsafe removes it, it does not effect the
| semantics.
| TheDong wrote:
| You're right that '[i]' is just a function call
| ('.index(i)' https://doc.rust-
| lang.org/std/ops/trait.Index.html).
|
| > So, for me, the placing of bounds checks when using
| that function is an implementation detail and therefore,
| if unsafe removes it, it does not effect the semantics.
|
| The function is not marked as unsafe, so it promises that
| it will not corrupt memory and thus must perform bound
| checks. The designation of safe/unsafe for a function is
| compile-time and promises certain semantics.
|
| It would be a semantic issue for a safe function to
| invoke unsafe behavior.
|
| Even within an 'unsafe' block, calling safe functions
| should not cause memory corruption as long as your other
| unsafe calls / unsafe code didn't do anything "wrong".
|
| Anyway, to implement a function like that, you'd need:
| fn index(i) -> T { if
| is_caller_in_unsafe_block() { return
| unsafe { unsafe_index(i) } } ... }
|
| The compiler does not, as far as I'm aware, have any
| "is_caller_in_unsafe_block" primitive, and adding one
| seems quite fraught.
| ArrayBoundCheck wrote:
| mtlmtlmtlmtl wrote:
| I've been thinking for some time that one of the key advantages
| of Rust's safe/unsafe code will turn out to be that formal
| methods can be applied to the unsafe parts.
|
| Safe Rust is truly safe if it only calls safe Rust or if all the
| unsafe code is correct.
|
| And safe Rust is a little too inflexible to do certain things, so
| the unsafe word is a necessary evil. But turns out it's not a
| bug, it's a feature because now you can trivially identify which
| parts of the codebase require extra scrutiny to avoid memory
| corruption and data races.
|
| With FM the main downside has always been the added cost and
| development time/complexity, needing to use obscure academically
| oriented systems that most developers have no experience with,
| etc. But that complexity is probably okay for a project like the
| Rust standard library, which is already a highly complex project
| and will only be majorly worked on by a relatively small subset
| of Rust developers. So you could save some of that cost by only
| needing it in a (relatively) small part of the ecosystem.
|
| Ofc I realise this wouldn't give the same level of correctness as
| doing all code with FM. You could only verify whatever guarantees
| Rust provides for code with no unsafe codepaths. And proofs can
| have bugs too. But still I think it could increase safety a lot.
| tialaramex wrote:
| The Rust standard library is quite big, not compared to Python
| obviously, but compared to the scale of things we'd usually
| apply formal methods to.
|
| It also relies heavily on stuff that's not Rust. For example
| it's one line in Rust to decide to suppose this whole file
| named "C:\myfile\stuff.txt" is UTF-8 text, so put it all into a
| String - obviously the standard library reflects the obvious
| ways that could fail, maybe there _is_ no such file, maybe it
| 's actually a JPEG and not UTF-8 text, maybe the file is so
| enormous it can't be represented in RAM on this (presumably
| 32-bit) computer - but it's relying on the operating system to
| actually have a working filesystem, you can't use formal
| methods to deal with such things.
|
| It could make more sense to do the same to Rust's core library:
| https://doc.rust-lang.org/core/
|
| Unlike std, core is mostly stuff the language itself assumes
| exists. Rust's fundamental types all have methods for example
| (e.g. 'x'.is_ascii() is true) unlike say C, and the
| implementation of (most of) those methods lives in core.
| mtlmtlmtlmtl wrote:
| Well, core is clearly the place to start, otherwise anything
| above it in the lib hierarchy would be on non-verified ground
| anyway. I think it would then be worthwhile to at least start
| on the alloc crate. A lot of the datastructures use quite a
| few unsafe concepts for optimisation and getting around the
| borrow-checker without having to resort to runtime checking.
| Formally verifying Vec, Hashmap and friends would obviously
| pay huge dividends across the entire rust ecosystem in terms
| of overall safety, and should be perfectly surmountable(at
| least modulo the behaviour of OS memory management). And
| there's no reason you couldn't do it module by module.
| benreesman wrote:
| Fantastic article. For auditory learners like me, this is an
| iconic talk in the OG "Advanced Topics in Programming Languages"
| series that Google used to do: https://youtu.be/h0OkptwfX4g
|
| It goes all the way from parametric polymorphism, up through
| Curry-Howard, and winds up at Girard-Reynolds. It was what got me
| passionate about type theory as a young lad.
| stepchowfun wrote:
| It's always a pleasant surprise to see people using Coq and other
| formal verification technology to build confidence in their ideas
| and algorithms. We need to stop producing buggy software! If this
| article gave you a thirst for interactive theorem proving and you
| want to learn it from the ground up, I've recently written a Coq
| tutorial [1] which covers topics like programming with dependent
| types, writing proofs as data, and extracting verified code. That
| repository also contains a handy tactic called `eMagic` [2] (a
| variant of another useful tactic called `magic`) which can
| automatically prove the theorem from the article.
|
| [1]
| https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...
|
| [2]
| https://github.com/stepchowfun/proofs/blob/56438c9752c414560...
| irsagent wrote:
| Could TLA+ do the same thing?
| homodeus wrote:
| A nice intro/showcase to Coq, I suppose. But the triviality of
| this frankly makes it difficult for me to understand what value
| this has and what it teaches us - we've just proven that one kind
| of syntax is equivalent to another, because of an intuitionistic
| tautology. What I'd like to know is what it would mean for the
| rust type system if this _weren 't_ true, and therefore, what is
| really the difference between rust opaque types and generics in
| function signatures other than syntactic, and their formulation?
| Tainnor wrote:
| Just noting that the statement in question is not only a valid
| proposition in intuitionistic logic, but also in classical logic.
| That's not really surprising, as classical logic can prove
| everything that intuitionism can prove, but it deserves to be
| called out, as it otherwise might seem more sophisticated than it
| is for people unfamiliar with the finer details of proof systems.
| Tainnor wrote:
| On a somewhat technical note, I think the author is being
| slightly imprecise, though in a way that will normally not trip
| up most people. The proof has to be understood either as a proof
| scheme in first order logic, in which case we _technically_ need
| a separate proof for each possible choice of predicates P and Q,
| or we have to implicitly quantify over P and Q, i.e. "for all P,
| for all Q", which leads us to second order logic, but in this
| case there is now a single proof (which is exactly what's the
| case when we're using Coq).
|
| At least that's the case in classical logic (which is enough to
| understand this article), I'm not knowledgeable enough about
| intuitionism to know whether it typically includes second-order
| quantification, but even in that it would probably be better to
| make the quantification explicit.
| mirekrusin wrote:
| Michael Clarkson of "OCaml Programming: Correct + Efficient +
| Beautiful" [0] fame is currently publishing series of lectures
| "Software Foundations in Coq" [1] (new ones appearing once a
| week?) as a companion to [2] which looks as great as OCaml
| series.
|
| [0]
| https://www.youtube.com/playlist?list=PLre5AT9JnKShBOPeuiD9b...
|
| [1]
| https://www.youtube.com/playlist?list=PLre5AT9JnKShFK9l9HYzk...
|
| [2] https://clarksmr.github.io/sf-
| lectures/textbook/lf/Preface.h...
| siraben wrote:
| The manual proof style was nice to see for pedagogical purposes,
| however it should be noted that the statement is just a
| intuitionistic tautology, so much so that the entire proof can be
| automated with the built-in firstorder tactic:
| Theorem impl_trait_transform: forall (Trait: Type -> Prop)
| (Result: Prop), ((exists t, Trait(t)) -> Result) <->
| (forall t, (Trait(t) -> Result)). Proof.
| firstorder. Qed.
| PoignardAzur wrote:
| I'm having some trouble understanding the article's formula; and
| honestly it's a little weird to see people complain about how
| trivial the proof is.
|
| Both this article and the article it quotes introduce the "(([?]
| x. P(x)) - Q) = ([?] x. (P(x) - Q))" formula with absolutely no
| additional explanation. I guess that's fine if the article are
| _meant_ for people with a mathematics background, but at someone
| who has always struggled with post-high-school-maths... what the
| hell?
|
| I understand what [?], [?], =, and - represent ("there exists",
| "for all", "equivalent" and "implies", respectively), but I have
| no idea how to parse the entire formula. What are P and Q?
|
| After multiple tries, I'm reading it as "saying that 'there
| exists a x such that P(x) is true' implies Q" being equivalent to
| "for all x, P(x) implies Q", with the idea that P and Q are
| arbitrary proposals or whatever the proper terms are... But
| still, just processing the logical reasoning in my head is tough.
|
| On the other hand "some types implement traits, and if a function
| expects a trait impl you can only pass it types that implement
| that trait" feels absolutely clear to me. It might be that Rust
| is good at breaking down math concepts into the essentials you
| need for programming. Or it might be that formal Math notation is
| not for me.
| Tainnor wrote:
| > Or it might be that formal Math notation is not for me.
|
| No, it just means that you haven't studied that notation. Like
| programming, being skilled at maths is not something you're
| just naturally gifted with. It has to be studied.
|
| The proof of the proposition in question is "trivial" in the
| sense that a first course in formal logic is more than enough
| to fully understand it, and that there is really no extra trick
| involved, basically the proof is as straightforward as it could
| be.
|
| I will agree that the article doesn't explain enough how the
| formula in question relates to type theory and Rust's type
| system in particular.
| Arnavion wrote:
| P and Q are propositions. P takes one parameter and Q takes
| none. For example P(x) might be "x is odd". The term `P(x)` by
| itself refers to P(x) being true.
|
| So `[?] x. P(x)` is read as "There exists an x for which P of x
| is true." or "There exists an x such that P of x is true."
|
| So `(([?] x. P(x)) - Q)` is read as "If there exists an x such
| that P of x is true, then Q is true."
|
| And `([?] x. (P(x) - Q))` is read as "For all x, if P(x) is
| true then Q is true."
|
| The `=` indicates that the left hand side is true if and only
| if the right hand side is true, or in other words that they're
| equivalent, which you can tell from the descriptions above that
| they are.
| throwaway17_17 wrote:
| Just a quick note, the symbol = is typically meant to stand for
| 'material implication' and would be better read as 'if and only
| if'. Or at least that is the 'normal' usage in the literature
| for intuitionistic logic. It doesn't really change your reading
| of it, but equivalent does not really capture the traditional
| meaning of material implication. It is more accurate to portray
| the logical sentence as valid with either implication in the
| first position. The two statements are not equivalent to each
| other, but the re-ordering of the implications would be, i.e.
|
| (([?] x. P(x)) - Q) = ([?] x. (P(x) - Q)) is equivalent to ([?]
| x. (P(x) - Q)) = (([?] x. P(x)) - Q)
| kelnos wrote:
| Regardless of the verification bit (which I didn't read, as it's
| a bit over my head), this is probably the best explanation I've
| read about the difference between `imp Trait` and `dyn Trait`.
| max_ wrote:
| I have been contemplating on learning TLA+. Could someone
| experienced with formal verification let me know what I could be
| missing by not learning something like Coq?
___________________________________________________________________
(page generated 2022-08-01 23:01 UTC)