The Subtle Power of Booleans: Programming with truth and statefulness | Hacker News Reader

The Subtle Power of Booleans: Programming with truth and statefulness

medium.com

73 pointsmbellotti10 comments

Funny, coincidentally I recently read a paper [0] arguing (among other things) that truth values should be completely removed--that for software engineering they are largely useless and cause mistakes.

The argument goes that a True False value will "mean" different things in a context, but then when trying to model a complex entity there are inevitably leakages of definitions.

For formal verification of existing Boolean logic, however, it reasons that "verifying" our truth values would be very helpful, by exploring and modeling the state space that is made up by the composition of multiple booleans. This is very interesting in that regard!

[0]: Formalizing common sense reasoning for scalable inconsistency-robust information integration using Direct Logic Reasoning and the Actor Model, Carl Hewitt. https://arxiv.org/pdf/0812.4852.pdf

> The argument goes that a True False value will "mean" different things in a context

Well, it is the same with numbers anytime they mean something in the real world. One would have to add "unit types" to numbers and check that x + y causes a type error when a "nr. of humans" is added to a "nr. of rainy days", to give an example. If that is represented by adding two integers there won't be an error. In software comparing apples and oranges works fine as long as you use numbers...

Database generated IDs are a great example. We often use integers because it is convenient - but there's no reason you should be able to add two together.

Isn't that the whole point of nominal type systems that you shouldn't be "comparing apples and oranges"

Yeah, but type systems are not fool proof. eg: I've seen plenty of Java code which blindly passes String objects around that eventually get parsed into json/int/long/etc. At that point, the type system has been silently circumvented.

"Nothing is foolproof given a sufficiently talented fool."

> CNF we would not say the Englishman lives in the red house we would say either the owner of the house is NOT the Englishman OR the house is red (which effectively means the same thing).

Effectively, maybe. Somebody might object that those two clauses (NOT the Englishman OR the house is red) can't be satisfied both at the same time - because not only the Englishman lives in the red house, also nobody else also lives there. So it's also true "NOT the Englishman IMPLIES the house is NOT red", "house is NOT red IMPLIES NOT the Englishman", neither of which is derivable from the original clause (CNF allows regular, "mathematical" understanding).

Confusingly headlined article is about bookean circuit satisfiability (SAT).

funfact: Boole titled his on book on his algebra "The Laws of Thought". AI & computation were old friends long before electro-computers.

Still on that subject: Russel&Norvig put a "planning algorithm" on the cover of their AI book. The algorithm is by Aristotle (De motu animalium).

Now, here's a great read. Loved it. I've used tla+ ... I'll give alloy a try too. I'm interested in anything else along these lines.

Reply on news.ycombinator.com