Remix.run Logo
comonoid 2 days ago

The book "Program = Proof" by Samuel Mimram starts with a formula which is true for all n below

n = 15 341 178 777 673 149 429 167 740 440 969 249 338 310 889

I don't think you can catch it with any test suite.

pdhborges 2 days ago | parent [-]

If you have an int32 or less you can!

jaggederest a day ago | parent [-]

And you'll rapidly return to proofs when your "function input" is something like a sequence of, say, ieee floating point numbers coming over the wire of possibly unbounded length. State machines with proofs that all the cases are handled are great.