-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
which proves that the storing operation always produces a validly ordered array. That's essentially a code proof of correctness for a recursive function The Boyer-Moore prover was able to grind out a proof of that without help. That was a long proof, too.
I submitted this to JACM. It was rejected, mostly for uglyness. The concept that you needed all this heavy machine-driven case analysis to prove a nice simple "axiom" upset mathematicians. Today it would be less of an issue. People are now more used to proofs that take a lot of grinding through cases.
You could build up set theory this way, via ordered lists, if you wanted.
So that's a classic of what happens if you take "equal" seriously.
[1] http://www-formal.stanford.edu/jmc/towards.pdf
[2] https://theory.stanford.edu/~arbrad/papers/arrays.pdf
[3] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...
[4] https://github.com/John-Nagle/nqthm
which proves that the storing operation always produces a validly ordered array. That's essentially a code proof of correctness for a recursive function The Boyer-Moore prover was able to grind out a proof of that without help. That was a long proof, too.
I submitted this to JACM. It was rejected, mostly for uglyness. The concept that you needed all this heavy machine-driven case analysis to prove a nice simple "axiom" upset mathematicians. Today it would be less of an issue. People are now more used to proofs that take a lot of grinding through cases.
You could build up set theory this way, via ordered lists, if you wanted.
So that's a classic of what happens if you take "equal" seriously.
[1] http://www-formal.stanford.edu/jmc/towards.pdf
[2] https://theory.stanford.edu/~arbrad/papers/arrays.pdf
[3] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...
[4] https://github.com/John-Nagle/nqthm