The point is to rarely if ever use =, and instead use approximation
-
-
It is also quantifying over arbitrarily bad continuous functions, which you never actually deal with
1 reply 0 retweets 0 likes -
Also e/d arguments are nicer if you think of them as error functions. Instead of Ae, Ed, you think of d:R+ -> R+ which takes an e and gives
1 reply 0 retweets 0 likes -
the corresponding required input variation to stay within e output error
1 reply 0 retweets 0 likes -
Replying to @ReferentOfSelf @St_Rev
Ok… I guess this is a matter of taste. I am not so afraid of tentacles that I feel a need to go to such lengths to avoid possible monsters.
1 reply 0 retweets 0 likes -
Replying to @Meaningness @St_Rev
It's also a matter of actually doing it on a computer. There's a reason why proof assistants are based in intuitionistic type theory
1 reply 0 retweets 0 likes -
Replying to @ReferentOfSelf @St_Rev
I’m missing a step there. Some proof assistants use regular fopc. What’s the advantage of intuitionistic logic?
2 replies 0 retweets 0 likes -
Replying to @Meaningness @St_Rev
Intuitionistic proofs are programs, classical ones are not. This makes it a total functional programming language (assuming consistency)
1 reply 0 retweets 0 likes -
Replying to @ReferentOfSelf @St_Rev
I have a bad feeling that the word “Haskell” is lurking somewhere near here
1 reply 0 retweets 1 like -
Replying to @Meaningness @St_Rev
haskell is not total and therefore trash :) more like Agda/Coq/Idris/Lean
1 reply 0 retweets 0 likes
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.