At Isabelle et Vincent, French Pastries Dazzle in an Unlikely Location https://www.diningandcooking.com/2026721/at-isabelle-et-vincent-french-pastries-dazzle-in-an-unlikely-location/ #an #at #dazzle #desserts #eater #et #FeaturedStories #francais #france #French #FrenchDesserts #FrontPage #in #isabelle #location #Pastries #reports #unlikely #Vincent
"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!
Isabelle and Doom Guy for Isabelle Day!!
#fanart #crossover #isabelle #AnimalCrossing #doom #doomslayer #anthro
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/
Tobias Nipkow and friends have been writing a book about Verified Functional Data Structures, using Isabelle/HOL. It's quite neat.
Some observations on working in a non-dependently typed functional programming language
In my current day job, I’m involved in the development of a research-based software tool, where the language being used is Haskell. While I can’t talk about the specifics of either the tool or the mathematics as yet, there was something interesting that we had to go through last month in the development process.
As far as I am aware, (core) Haskell uses the type theory System FC, which is not dependently typed (I’m not a type theorist, and certainly not a PL theorist! The details are not critical for what follows in any case, so be gentle). So when we are implementing data structures that might be more naturally encoded in a dependently-typed system, we instead have validity checks which verify if the various constraints are satisfied or not. In practice, the functions that produce and manipulate these data types are intended to only ever produce objects that satisfy the constraints, but this isn’t enforced by the type system. Earlier in the year, in a previous version of the code, we had a working construction that manipulated some data to produce new data of the same type, and then we re-implemented the prototype software based on richer theoretical foundations, where the types carried more information, and the validity checks then had more work to do.
In testing this new version, once it was mature enough to do so, using Hedgehog, we were running into weird corner cases whereby our function was failing to return a valid object according to the validity tests. There was indeed a bug in the code, because the mathematical definition of the operation was a naive adjustment from the previous iteration. So ensued some time of panic whereby I had to find the correct definition of the data type as well as of the construction underlying the function.
To provide a strong level of confidence, we used Isabelle to formalise candidate mathematical definitions underlying our type (or rather the validity check), and the construction. I found it slightly ironic that in trying to verify the correctness of the mathematics of one non-dependently typed language we turned to another one. But the automation in Isabelle allowed me, a complete novice in formal verification, to break down my proofs into baby steps and supply lots of fairly obvious lemmas so that Sledgehammer tools could fill in the proofs, without having to fight the formalism. Were I someone with lots of time on my hands, I would learn Lean as well.
The Isabelle implementation of the prerequisite mathematical ideas was thankfully not horrible (and mostly handled by my colleague, who has more Isabelle experience than me, i.e. a nonzero amount!) and then we could thrash out exploring the design space of plausible definitions. This might seem a little odd, but since what we are developing is using research we are doing as we go, it’s not always clear what the right choices are, until we implement things and see what happens. Thankfully, we found a robust definition that also makes conceptual sense (and, of course, in hindsight, it’s exactly the right thing), and moreover which makes all the operations we want work, once they are suitably defined.
Another thing which I’ve come to appreciate is that in testing our definition, we had a complete formalisation of what amounts to something like a terminal object in some category. And to prove this really is an object of the mathematical sort we are thinking of was hundreds of lines of Isabelle. (This reminds me of Buzzard et al’s formalisation of a perfectoid space, even if not of the same scale, and then the only example they formalise is the empty space!) What this additionally gave us is that the axioms that are encoded in the validity checks on our data structure are well-typed, for the general case. That is, we ask, for example, that some operation is associative, but this is an operation on indexed data, and so the equality in the associativity law has the potential to be trying to equate objects of different types, were we in a fully-fledged dependently-typed system. But since we weren’t, everything has to be packaged up together in a single type and checked post-hoc.
I’m aware there is work on at least simulating dependent types in Haskell, current work on trying to actually implement dependent types in an extension to Haskell, and for that matter, languages that are based on dependent type theories, but until one of these is performant enough and has enough library support so as to write production code in, we are stuck with what we have (and this is also informed by the expertise of the people involved, to which I add relatively less on the coding side). Being able to work in a dependently-typed language would mean that the type system would take care of ensuring the operations are well-typed as mathematically intended, but certainly having to work in this setting makes things interesting, in trying to work around the limitations of the type system and be confident in the result.
Aquest any fa 25 anys que ens arribava "Isabelle" per "Windows" 
. #Isabelle #Windows #Aventura #Videojocs #Gaming #VideoGames #RetroGaming #ClassicGaming #RetroGames #VideojocsAntics
My PhD student Sára and I are looking for people to participate in a study on usability aspects of interactive theorem provers. Please consider signing up!
Who? anyone who uses or has used an interactive theorem prover for whatever purpose
What? 90 - 120 minute interviews (possibly including a small think-aloud programming session)
When? interviews will be scheduled starting September 2024
Where? online (participants from anywhere are welcome)
We are hoping these interviews will help us determine how you interact with your theorem provers and to gain insights on how we can improve the user experience. We are interested in all aspects of interactive theorem provers, including but not limited to their design, their tooling, their libraries, and their documentation.
Sign up here: https://tudelft.fra1.qualtrics.com/jfe/form/SV_0UJKuqcWC9G4FEy
IsarMathLib 1.30.0: Modules and update to Isabelle2024. https://slawekk.wordpress.com/2024/05/28/isarmathlib-1-30-0-modules-and-update-to-isabelle2024/ #ITP #Isabelle #Math
Nachan 
