Skip to content

Instantly share code, notes, and snippets.

@viniciusd
viniciusd / rust1plus1.md
Created November 11, 2021 18:54 — forked from gretingz/rust1plus1.md
Proving that 1 + 1 = 2 in Rust

Proving that 1 + 1 = 2 in Rust

The fact that 1 + 1 is equal to 2 is one of those things that is so obvious it may be hard to justify why. Fortunately mathematicians have devised a way of formalizing arithmetic and subsequently proving that 1 + 1 = 2. Natural numbers are based on the Peano axioms. They are a set of simple rules that define (along with a formal system) what natural numbers are. So in order to prove 1 + 1 = 2 in Rust we first need a formal system capable of handling logic. The formal system that we'll be using is not some random crate, but Rust's type system itself! We will not have any runtime code, instead the type checker will do all the work for us.

Implementing the Peano axioms

First let's go trough the Peano axioms. The first axiom is that "Zero is a natural number". Basically what it says is that zero exists. In order to express that in the type system, we just write:

-module(billing).
-export([print_bill/1]).
database() ->
[
{1111, "Hula Hoops", 21},
{1112, "Hula Hoops (Giant)", 133},
{1234, "Dry Sherry, 1lt", 540},
{4719, "Fish Fingers" , 121},
{5643, "Nappies" , 1010},
The heat bloomed in December .VB
as the carnival season .CV
kicked into gear. .LP
Nearly helpless with sun and glare, I avoided Rio's brilliant .RP
sidewalks
and glittering beaches,
panting in dark corners
and waiting out the inverted southern summer. .JU
-module(tail_recursion).
-export([is_perfect/1]).
is_perfect(N) ->
2*N == lists:sum(divisors(N)).
divisors(N) ->
divisors(N, 1, []).
divisors(N, I, ACC) when I*I < N andalso N rem I == 0 ->
divisors(N, I+1, [I|[N div I|ACC]]);
@viniciusd
viniciusd / joining.erl
Created May 24, 2020 22:39
3rd section of the 2nd week of the Functional Programming in Erlang from the University of Kent
-module(joining).
-export([join/2, concat/1]).
reverse([X|Xs]) -> reverse(Xs, [X]);
reverse([]) -> [].
reverse([X|Xs], ACC) -> reverse(Xs, [X | ACC]);
reverse([], ACC) -> ACC.
shunt([],Ys) ->
Ys;
-module(exercises).
-export([maximum/1,double/1,evens/1, median/1, modes/1]).
maximum([X|Xs]) -> maximum(Xs, X).
maximum([X|Xs], ACC) -> maximum(Xs, max(X, ACC));
maximum([], ACC) -> ACC.
double([X|Xs]) when is_number(X) -> double(Xs, [2*X]).
double([X|Xs], ACC) when is_number(X) -> double(Xs, [2*X|ACC]);
use hyper::{self,Client};
use hyper::rt::{self,Future,Stream};
use hyper_tls::HttpsConnector;
use std::fs::File;
use std::io::prelude::*;
use futures::future;
from datetime import datetime
import logging
import os
import subprocess
logger = logging.getLogger(__name__)
class TcpDump:
def __enter__(self):
now = int(datetime.now().timestamp())
import java.util.function.Function;
public class MyClass {
private static Function<Integer,Integer> outside(Integer y) {
return new Function<Integer, Integer>() {
@Override
public Integer apply(Integer x) {
return x + y;
}
CREATE OR REPLACE FUNCTION pivot(
refcursor, tablename character varying,
rowc character varying,
colc character varying,
cellc character varying,
celldatatype character varying)
RETURNS refcursor
LANGUAGE 'plpgsql'
COST 100