5 ms·
Proving that 1 and 1 = 2 in Rust
- klyrs 6y agoTitle is awful. 1 and 1 is 1; 1 plus 1 is 2.
- panopticon 6y agoUsing "and" like this is a common shorthand for "the sum of n and m is...". The shorthand is a bit antiquated now, but you can find it in a lot of arithmetic books (and song lyrics).
- klyrs 6y agoMiss me with that "common usage" on this article for and by programmers.
- kevincox 6y agoI was confused because I thought they were proving that (1 = 1) and (1 = 2).
- contravariant 6y agoThat's fine but if half of it is in symbolic notation and the rest is in prose you can't blame people if they group the symbolic part together.
- brundolf 6y agoI assumed it was a workaround for some title-formatting rule that HN has, given that the original article uses +
- auroranil 6y agoThen why not use word "plus" instead? "Proving that 1 plus 1 = 2 in Rust" is a more suitable title that does not use symbol +.
- jwilk 6y agoAIUI, it was not the submitter who rewrote the title; HN did it automatically. See https://news.ycombinator.com/item?id=14944003 https://news.ycombinator.com/item?id=14944003 for another submission that had this issue.
- leetcrew 6y agoit's pretty clear from context that we're talking about addition. you don't usually see '2' on the RHS of a boolean equation.
- klyrs 6y agoTo the contrary, 7 and 10 is 2
- DarthGhandi 6y agoYou do in bitwise AND calculations.
- alblue 6y agoThe linked article has 1+1=2; the title in HN is incorrect but may have prevented the use of the + symbol.
- 7373737373 6y agoHere in the Metamath proof verification system: http://us.metamath.org/mpegif/1p1e2.html http://us.metamath.org/mpegif/1p1e2.html More interestingly, 2+2=4: http://us.metamath.org/mpegif/2p2e4.html http://us.metamath.org/mpegif/2p2e4.html (also have a look at the trivia: http://us.metamath.org/mpeuni/mmset.html#trivia http://us.metamath.org/mpeuni/mmset.html#trivia !)
- im3w1l 6y agoIt's a bit confusing to see a proof not even mentioning successor and relationship to addition.
- brundolf 6y ago*in Rust's type system
- amelius 6y agoUgh this makes me think of the Boost template hacks.
- Tainnor 6y agoIt's quite cool that you can use type systems in "regular" languages to do such things. Notice though, that this system is not powerful enough to prove all the facts about the natural numbers. For example, the author states that this system has the property that there is no number smaller than zero. This is true, at least if we define "smaller than" transitively via the successor function (/ type constructor). However, it's still entirely possible to define a "struct NegativeOne();" and define addition so that -1+1=0, so you can't prove that there is no number such that when you add to it a nonzero number, you get zero. More generally, this system doesn't actually formally define the natural numbers, it just constructs a finite number of them (which is fine, the article didn't claim otherwise). I don't know if Rust's type system is powerful enough to construct the natural numbers in some "natural" way (it's mentioned that the type system is Turing complete, but that doesn't technically guarantee that such an encoding would be practical to use), you'd need some way of writing an inductive type definition where Zero is a Nat and Succ<N> is a Nat iff N is s Nat. You can do such things in theorem provers, here's a tutorial on how to do it in Lean: https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam...
- gepoch 6y agoNo system is powerful enough to prove all of the facts about natural numbers, right?
- Tainnor 6y agoI think that this is correct and a consequence of Gödel's incompleteness theorems, although my knowledge about this is quite sketchy. What I was referring to more (and should have clarified better) was that there are models of arithmetic that can characterise the natural numbers uniquely (up to isomorphism) - translated to type theory, it is possible in languages like Coq and Lean to fully define what a natural number is without including any extra objects - even if you won't be able to prove all theorems about them. Notably, though, first order theories are not sufficient to define the natural numbers, for every set of first-order axioms about the natural numbers, there are "non-standard models" that can look quite weird. You need second-order logic or something equivalent in power to prevent that (the difficult axiom here is the axiom of induction which needs to be able to quantify over predicates).
- moasda 6y agoNice to see that somebody implements the Peano axioms to do calculation and proofs.