My wife [watching The Phantom Menace with me]: they really like fighting next to holes
Me: well, that’s the price. You have really cheap and reliable AI, you have warp drive that’s cheap and powerful enough to politically unify a galaxy, but there’s holes everywhere.

#starwars #høl

#365rpgbooks Day 49 - HoL (Human occupied Landfill) #pnpde #rpg #hol

For HOL, the axiom of infinity (and I guess Hilbert's operator) gives it its strength. Can we replace it with a weaker alternative? Can we get something as weak as, say, PRA?

#ProofAssistant #HOL #mathematics

just found from researchgate

#metaphysics #ontological_proof
#modal_logic #HOL #Kurt_Gödel #Dana_Scott

this open access paper may be of interest to rather everyone in the field

https://link.springer.com/article/10.1007/s00605-025-02078-x

I like the idea of a reformed House of Lords being full of experts in their field, so they knock back populist shit like this.

#UKPOL #Ukpolitics #HoL #Law

If you are trying to get HOL4 working on a Raspberry Pi, you need to use MoscowML.

Poly/ML native compilation is not really supported for Raspberry Pi, and its bytecode interpreter performs worse than MoscowML's bytecode interpreter anyways.

I learned this after spending a few frustrating days trying to get PolyML to build HOL4, fruitlessly, then gave Mosml a shot (and it worked like a charm).

The things you learn...

#HOL #MoscowML #PolyML #StandardML #RaspberryPi

I am sad so few proof assistants use IRC.

Does #HOL use it? I can't find a channel on libera.chat; #isabelle uses irc. But HOL Light? HoL Zero?

I don't think so, and it depresses me quite a bit.

New Artist announced for Sziget Festival 2025: 🔥 Hol! 🔥

🎶 Listen to the current LineUp on YouTube and Spotify: https://fyrefestivals.co
🎟️ Get your Tickets now: https://prf.hn/l/EJnYMdO

#Sziget_Festival_2025 #Hol #fyre_festivals #livemusic #youtube #spotify #music #musicfestivals #playlist #tickets #announcement

And this is why people think Labour are not on their side

#UKPOL #UKpolitics #Labour #HoL #NICBill

More of this sort of thing

Americans, imagine if the Senate weren't elected but appointed by the Government and you had Hereditary Senators dating back way too long ago, and 'Lords Spiritual'.....well you're kinda heading there now really,so....

https://www.theguardian.com/politics/2025/mar/20/lords-out-people-in-protesters-interrupt-proceedings-in-house-of-lords

#HoL #UKPOL #UKpolitics

Corruption for foreign nations is treason.
But only if you're poor and don't have the right friends, obviously....

https://www.theguardian.com/politics/2025/mar/10/foreign-states-repressive-regimes-pay-peers-over-3m-two-years

#UKPOL #UKpolitics #Corruption #HoL

Imagine being so fucking racist, you'd Protest Vote for a traitor who will sell out this country to Russia and America.

How many Russian assets are in the House of Lords btw?

#NigelFarage #ProtestVote #Oligarchs #Treason #UKPOL #UKpolitics #HoL

New Artist announced for Parookaville Festival 2025

HOL!

Added top 5 songs to the playlist Parookaville Festival 2025

Listen now on YouTube Music: https://www.youtube.com/playlist?list=PLB5UNN-XlHr0umrk0ra5F0YQEkwaw4xBJ

#Parookaville_Festival_2025 #HOL! #fyre_festivals #livemusic #youtube #music #2025 #musicfestivals

Another project idea: formalize the semantics of HOL in Mizar.

This is actually quite straightforward, since Andrew Pitts formalized most of the work back in his 1991 presentation of HOL's semantics.

But I don't think it's been formalized! Perhaps it has, I don't know, I wrote this up as the city I live is engulfed in flames: I didn't have the luxury of time to find out.

But that shouldn't stop you from having fun! There are a million variations to consider, as well: typeclasses, inductive types, etc. etc. etc.

#Mizar #HOL #ProofAssistant #Semantics

https://thmprover.wordpress.com/2025/01/14/hol-in-mizar/

Kick shirkers out of the House of Lords!
act.38degrees.org.uk/act/hol-s…

#HOL
#Lords

Kick shirkers out of the House of Lords! act.38degrees.org.uk/act/hol-shir... #HOL #Lords

Sign the petition if you agree...

Kick shirkers out of the House of Lords!
https://act.38degrees.org.uk/act/hol-shirkers-lbda?bucket=instagram-post-10_12_2024_shirkers_Th01&utm_campaign=10_12_2024_shirkers_Th01&utm_medium=post&utm_source=instagram

#HOL
#Lords

【宝鐘マリン1stライブ「Ahoy!! キミたちみんなパイレーツ♡」】みんなで同時視聴！！【火威青 /音乃瀬奏/響咲リオナ/虎金妃笑虎】#hol... https://youtube.com/live/7jf3nH21rbA?si=eMgQQjaTAvmykq1Y

どうせ内容はあとからbilibiliに上がるんだろうから(苦笑)、今はホロライブデバイスの面々の反応を見てみたい。
JPメンの反応よりは新鮮に見れそう。
FLOWGLOWの初配信も、自分はリグロスの同時視聴枠で見ていた。

IPP sentence: Top judge demands help for prisoners ‘left to rot’ under ‘morally wrong’ indefinite jail terms | The Independent
https://www.independent.co.uk/news/uk/crime/ipp-sentence-lord-thomas-prison-b2631771.html

#HOL
#IPP
#IndefiniteJailTerms

I want to see real reform to the House of Lords: including no more party donors being given a place, and a retirement age for sitting members. Agree we need to see bold change? Sign the petition now!
https://act.38degrees.org.uk/act/reform-the-house-of-lords-petition?bucket=copy-native-2024-09-05_&utm_campaign=2024-09-05_House+of+Lords+reform+2024&utm_medium=native&utm_source=copy

#HOL
#HOLReform
#UKPolitics
#Parliament