"How do you test?"
.. was an interesting question at last night's #pydata Exeter where 2 of the 3 talks were on proof assistants - mine on Lean, another on Isabelle.
The answer is surprising to newcomers.
The only error you can make is in incorrectly specifying the thing you want to prove. You don't make mistakes in the proof itself.
Pretty cool!
VINTAGE POSTCARD Attelage Streaks has Robe Isabelle rayee brown Africa Zoological gardens Paris
https://www.cpaphil.com/en/categories/teams/pages/4
#Attelage #Streaks #Robe #Isabelle #Rayee #Brown #Africa #ZoologicalGardens #Paris #VintagePostcard #History #Heritage
#HistoricalPostcard
I forgot to share this one. Gonna just post the Fur Affinity link this time.
𝗦𝘁𝗼𝗽𝗽𝗲𝗻 𝗺𝗲𝘁 𝗺𝗼𝗽𝗽𝗲𝗿𝗲𝗻: 𝗜𝘀𝗮𝗯𝗲𝗹𝗹𝗲 𝗽𝗹𝗲𝗶𝘁 𝘃𝗼𝗼𝗿 30 𝗱𝗮𝗴𝗲𝗻 𝘇𝗼𝗻𝗱𝗲𝗿 𝗸𝗹𝗮𝗴𝗲𝗻
Het is koud, grijs, de dagen zijn te kort en alles is te duur. Op deze 'Blue Monday' ligt het voor de hand om even flink te mopperen. Maar we zouden eens moeten proberen om een maand niet te klagen. Althans dat vindt de Belgische Isabelle Gonnissen oprichter van de campagne '30 dagen zonder...
https://www.rtl.nl/nieuws/editienl/artikel/5490348/30-dagen-zonder-klagen-mopperen
Isabelle and Doom Guy for Isabelle Day!!
#fanart #crossover #isabelle #AnimalCrossing #doom #doomslayer #anthro
Robo Isabelle, patreon art!
Commissions in this style are available, $70 a character, DM if you're interested!
#art mastoart #robot #furry #animalcrossing #isabelle #commissionsopen #commissions
Running the manual: an approach to high-assurance microkernel development
> the kernel is obviously a state
transformer, and hence, conveniently represented as a monad. This
choice is reaffirmed by the need for recoverable exceptions, which
are detailed in the next subsection. In fact, we will see that we want
to distinguish between code that may raise recoverable exceptions
and code that does not have that liberty. Hence, it is worthwhile
to use monad transformers as provided by the MTL in the Haskell
Hierarchical Libraries
> seL4 API includes several system calls that
attempt to manipulate a capability address space, which is a data
structure containing a sparse mapping from addresses to capabili-
ties. If one of these system calls fails to locate a specified capability,
it will generate a system call error that is returned to the caller. On
the other hand, a similar failure while searching for a capability that
is being directly invoked will generate a fault message that is sent
to the current thread’s fault handler; a failure while trying to trans-
mit a capability through a one-way communication channel will be
silently ignored when the receiver is unable or unwilling to receive
the capability.
> HOL is a logic of total functions and is as such not suitable to ex-
press the semantics of Haskell directly. It is however suitable to
describe the semantics of Haskell functions that always terminate
and that do not make essential use of laziness. The seL4 implemen-
tation consists of such functions.
#haskell #isabelle #sel4
http://portal.acm.org/citation.cfm?id=1159842.1159850&coll=portal&dl=ACM&type=series&idx=1159842&part=Proceedings&WantType=Proceedings&title=Haskell&CFID=18785943&CFTOKEN=93152956
What is a "structure" in Mizar?
This was always one of the most confusing things to me when I first got started with #Mizar since the answer requires a little bit of Model Theory, which isn't adequately taught in the US to "generic Mathematicians".
The answer is surprisingly deep yet simple: it's "just" a finite partial map in the Metatheory. This can be made precise using something like #Isabelle as the Metatheory (as done in the Isabelle/Mizar project).
We can also use a finite set of "attribute"-value pairs, which is called "first-class aggregates" (or "first-class structures") since they're defined like any other notion in Mizar, without special metatheoretic considerations. And they're useful for doing graph theory!
#Mizar #ProofAssistant #ModelTheory #Model_Theory #Logic #Mathematics
https://thmprover.wordpress.com/2024/10/04/what-is-a-structure-in-mizar/
Some observations on working in a non-dependently typed functional programming language
#LeMonde : "Au #théâtre, le retour d’une #censure qu’on croyait évanouie"
"A la différence de #SylvieChalaye, l’universitaire #Isabelle# Barbéris ne fait pas de distinction : « Les #censures de #droite et de #gauche ont tendance aujourd’hui à se recouper…[autant] la censure qui défendrait la juste représentation de #minorités dominées » que « celle émanant de groupements d’intérêts #réactionnaires et #conservateurs »."
-Closed!]
Nachan