@jonny funny thing, but a number of people in the theorem...

jonny (good kind)'s posts Post Back to profile

@jonny funny thing, but a number of people in the theorem prover community think we should stop using bools and replace them with proofs and contradictions

Like 26 April at 8:40 | Wall-to-wall | Open on social.treehouse.systems

7 comments

f.rift :fire_blue:

@dysfun @jonny makes sense; nothing in math is true or false, only consistent or inconsistent.

26 April at 9:13 | Open on hackers.town

f.rift :fire_blue:

@dysfun @jonny (or underspecified for the determination of its consistency. or, uh, some worse things that can occur in special cases...)

26 April at 9:14 | Open on hackers.town

gaytabase

@feonixrift @jonny we tend to think of it as booleans erasing what they pertain to :)

26 April at 9:14 | Open on social.treehouse.systems

f.rift :fire_blue:

@dysfun @jonny so booleans are a form of money?

26 April at 9:15 | Open on hackers.town

gaytabase

@feonixrift @jonny you want coin-operated computation? we can do that! https://www.idris-lang.org/docs/idris2/current/base_docs/docs/Data.Fuel.html

26 April at 9:17 | Open on social.treehouse.systems

f.rift :fire_blue:

@dysfun @jonny :blobsweats: I don't think I have time to esolang rabbithole today.

26 April at 9:19 | Open on hackers.town

gaytabase replied to f.rift

@feonixrift @jonny it's not esoteric, it's just type theoretic

26 April at 9:20 | Open on social.treehouse.systems

Go Up