BreakfastB0b

Error/Either monads are the perfect middle ground IMHO. You get errors as data types and an efficient way to abstract away the boilerplate associated with it.

50+ Real-World Blockchain Use Cases that all involve some kind of trusted party thus invalidating the whole point of using a blockchain in the first place. Call me when you have a solution to the Trustless Oracle Problem. Until then just use a fucking database.

“The Myth of Sisyphus” by Albert Camus, if you find yourself worrying about existential nihilism then this is the book for you. I found it extremely useful after an intense psychedelic experience. The School of Life has a good overview of his brand of existentialism here https://youtu.be/jQOfbObFOCw

I haven't got up to proving things about floating point numbers in Coq. But my guess would be probably not.

But Haskell's quickCheck doesn't seem to find a problem.

  λ quickCheck @(Float -> Bool) $ \x -> 2 * x == x + x
  +++ OK, passed 100 tests.
  λ quickCheck @(Double -> Bool) $ \x -> 2 * x == x + x
  +++ OK, passed 100 tests.

It doesn't like associativity though.

  λ quickCheck @(Double -> _) $ \a b c ->
    (a + b) + c == a + (b + c)
  *** Failed! Falsifiable (after 6 tests and 4 shrinks):
  20.0
  3.5741489348898856
  2.894651135185324

One way is to use Functional Extensionality, which is to say that two functions are equal if for all possible inputs they return the same value.

In Coq for instance.

  Axiom functional_extensionality: forall {X Y: Type} {f g : X -> Y},
    (forall (x: X), f x = g x) -> f = g.

  Theorem x2_eq_xplus:
    (fun x => 2 * x) = (fun x => x + x).
  Proof.
    apply functional_extensionality. intros.
    destruct x.
    - reflexivity.
    - simpl. rewrite <- plus_n_O. reflexivity.
  Qed.