Proving that 1 and 1 = 2 in Rust | Hacker News Reader

Proving that 1 and 1 = 2 in Rust

gist.github.com

31 pointsagluszak22 comments

Title is awful. 1 and 1 is 1; 1 plus 1 is 2.

Using "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).

Miss me with that "common usage" on this article for and by programmers.

I was confused because I thought they were proving that (1 = 1) and (1 = 2).

That'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.

I assumed it was a workaround for some title-formatting rule that HN has, given that the original article uses +

Then why not use word "plus" instead? "Proving that 1 plus 1 = 2 in Rust" is a more suitable title that does not use symbol +.

AIUI, it was not the submitter who rewrote the title; HN did it automatically.

See https://news.ycombinator.com/item?id=14944003 for another submission that had this issue.

it's pretty clear from context that we're talking about addition. you don't usually see '2' on the RHS of a boolean equation.

To the contrary, 7 and 10 is 2

You do in bitwise AND calculations.

The linked article has 1+1=2; the title in HN is incorrect but may have prevented the use of the + symbol.

Here in the Metamath proof verification system: http://us.metamath.org/mpegif/1p1e2.html

More interestingly, 2+2=4: http://us.metamath.org/mpegif/2p2e4.html

(also have a look at the trivia: http://us.metamath.org/mpeuni/mmset.html#trivia !)

It's a bit confusing to see a proof not even mentioning successor and relationship to addition.

It'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_gam...

No system is powerful enough to prove all of the facts about natural numbers, right?

I 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).

Ugh this makes me think of the Boost template hacks.

Nice to see that somebody implements the Peano axioms to do calculation and proofs.

*in Rust's type system

Which was implemented under the assumption that 1+1=2

No, that's a consequence of the Peano axioms. 1 and 2 are just a short notation of S(0) and S(S(0)), respectively.

Reply on news.ycombinator.com