my forest
forgot to push isa stuff
+121
-4
assets/clear1.jpeg
assets/clear1.jpeg
This is a binary file and will not be displayed.
assets/clear2.jpeg
assets/clear2.jpeg
This is a binary file and will not be displayed.
+3
-2
trees/isa/isa-0001.tree
+3
-2
trees/isa/isa-0001.tree
···
1
-
\title{Introduction to Interactive Theorem Proving}
1
+
\title{Introduction to Interactive Theorem Proving (Draft)}
2
2
\author{liamoc}
3
3
\taxon{Lecture Notes}
4
-
\p{These notes are the basis of my short course at the [ANU Logic Summer School]() 2025.}
4
+
\p{These notes are the basis of my short course at the [ANU Logic Summer School]() 2025. \strong{THEY ARE NOT YET COMPLETE.}}
5
+
\transclude{isa-0002}
+2
-1
trees/isa/isa-0003.tree
+2
-1
trees/isa/isa-0003.tree
···
3
3
\title{Isabelle and HOL}
4
4
\<html:img>[width]{250px}[class]{portrait}[style]{border:0px}[src]{\route-asset{assets/isabelle_hol.svg}}{}
5
5
\p{These lectures introduce theorem proving using the proof assistant [Isabelle](https://isabelle.in.tum.de/). Isabelle supports many logics, but by far the most popular is \strong{H}igher \strong{O}rder \strong{L}ogic, the focus of these notes. Isabelle comes pre-packaged with its HOL libraries, as well as a proof editor (based on jEdit) and various other tools. }
6
-
\p{The proof developments shown in these notes are all developed with Isabelle 2024, but Isabelle 2025 (the latest version at time of writing) is largely backwards compatible with it. I have not upgraded due to some proof automation regressions in Isabelle 2025 that do not affect the content of these notes.}
6
+
\p{The proof developments shown in these notes are all developed with Isabelle 2024, but Isabelle 2025 (the latest version at time of writing) is largely backwards compatible with it. I have not upgraded due to some proof automation regressions in Isabelle 2025 that do not affect the content of these notes.}
7
+
\transclude{isa-0013}
+12
trees/isa/isa-0012.tree
+12
trees/isa/isa-0012.tree
···
1
+
\date{2025-11-30T11:47:22Z}
2
+
\author{liamoc}
3
+
\title{Installing Isabelle/HOL on Windows}
4
+
\ol{
5
+
\li{Go to the [official Isabelle downloads page](https://isabelle.in.tum.de/download.html)}
6
+
\li{Download the Windows installer (a \code{.exe} file).}
7
+
\li{Run the downloaded file.}
8
+
\li{Choose where you want Isabelle to be installed (the default is fine).}
9
+
\li{After installation, open the folder where Isabelle was placed (e.g. \code{C:/Isabelle2024}).}
10
+
\li{Inside the bin subfolder, double-click
11
+
\code{isabelle_jedit.exe}. This launches the Isabelle/jEdit IDE.}
12
+
}
+4
trees/isa/isa-0013.tree
+4
trees/isa/isa-0013.tree
+11
trees/isa/isa-0014.tree
+11
trees/isa/isa-0014.tree
···
1
+
\date{2025-11-30T11:47:25Z}
2
+
\author{liamoc}
3
+
\title{Installing Isabelle/HOL on macOS}
4
+
\ul{
5
+
\li{Go to [the Isabelle download page](https://isabelle.in.tum.de/download.html).}
6
+
\li{
7
+
Download the macOS DMG file.}
8
+
\li{Open the DMG.}
9
+
\li{Drag the Isabelle application into your Applications folder.}
10
+
\li{Open Applications → Isabelle to start the Isabelle/jEdit IDE.}}
11
+
\em{(If macOS warns that the app is from an unidentified developer, go to System Settings → Privacy & Security and approve it.)}
+10
trees/isa/isa-0015.tree
+10
trees/isa/isa-0015.tree
···
1
+
\date{2025-11-30T11:47:25Z}
2
+
\author{liamoc}
3
+
\title{Installing Isabelle/HOL on Linux}
4
+
\ul{
5
+
\li{Go to [the Isabelle download page](https://isabelle.in.tum.de/download.html).}
6
+
\li{
7
+
Download the Linux tar.gz bundle.}
8
+
\li{Extract it with: \code{tar -xzf Isabelle2024_linux.tar.gz}}
9
+
\li{Open the extracted folder.}
10
+
\li{Start the Isabelle/jEdit IDE with: \code{./bin/isabelle jedit}}}
+1
-1
trees/loc-000P.tree
+1
-1
trees/loc-000P.tree
···
9
9
10
10
\p{In 2022 I visited the monks at the [Abbaye Saint-Pierre de Solesmes](https://www.solesmes.com/), under Dom Geoffrey Kemlin. In Edinburgh I sang with the the Choir of [St. Michael and All Saints](https://smas.church/) Episcopal Church. I am a member of the [Royal School of Church Music](https://rscmaustralia.org.au/).}
11
11
12
-
\p{In particular, I have an interest and considerable expertise in the rich chant tradition of the medieval western church, and I am seeking rare prayer books, hymnals, graduals, nocturnals, vesperals, diurnals, antiphonaries and similar.}
12
+
\p{In particular, I have an interest and considerable expertise in the rich chant tradition of the medieval western church, and I am seeking rare prayer books, hymnals, graduals, nocturnals, vesperals, diurnals, antiphonaries and similar. Details of my musical score collection are maintained in my [[loc-002D]].}
13
13
14
14
\p{Below you will find mostly-weekly entries, journaling my liturgical and music experiences.}
15
15
\query\datalog{
+1
trees/loc-001B.tree
+1
trees/loc-001B.tree
+26
trees/loc-002I.tree
+26
trees/loc-002I.tree
···
1
+
\import{table-macros}
2
+
\def\percent{\startverb%\stopverb
3
+
}
4
+
\parent{loc-000P}
5
+
\title{1st Sunday of Advent 2025}
6
+
\tag{cmc}
7
+
\date{2025-11-30}
8
+
\author{liamoc}
9
+
\quote{
10
+
Ad te levávi ánimam méam: Déus méus in te oncido, non erubéscam: neque irrídeant me inimíci mei: étenim univérsi qui te expéctant, non confundéntur.}
11
+
\p{This Sunday at [All Saints Ainslie](https://allsaintsainslie.org.au) we were almost pre-warmed up from our rehearsal yesterday (for next week's Carol service). We sang Waters' lovely short anthem [I sing of a maiden that is mateless](https://www.youtube.com/watch?v=s6uU6lk4kd4):}
12
+
\quote{
13
+
\poem{
14
+
\line{I syng of a mayden þat is makeles,}
15
+
\line{kyng of alle kynges to here sone che ches.}
16
+
\line{He came also stylle þer his moder was}
17
+
\line{as dew in aprylle, þat fallyt on þe gras.}
18
+
\line{\br}
19
+
\line{Moder & mayden, was neuer non but che –}
20
+
\line{wel may swych a lady, Godes moder be.}
21
+
}
22
+
}
23
+
\p{I am starting to organise a group of monthy Evensong singers for next year. If you want to contriubte your voice, please get in touch with me!
24
+
}
25
+
\p{Also, as I recently got a collection of Tallis anthems to add to my [score collection](loc-002D), I sang through a verse of \em{Why fum'th in sight}, the anthem that would, long after its writing, be rediscovered by Ralph Vaughan Williams and inspire his beautiful Fantasia for string orchestra.}
26
+
\<html:iframe>[style]{aspect-ratio: 16 / 9;}[width]{100\percent}[src]{https://www.youtube.com/embed/F4LHpA5PWKg}[title]{Why Fum'th in Sight}[frameborder]{0}[allow]{accelerometer; autoplay; clipboard-write; encrypted-media; gyroscope; picture-in-picture; web-share}[referrerpolicy]{strict-origin-when-cross-origin}{}
+4
trees/loc-002J.tree
+4
trees/loc-002J.tree
···
1
+
\date{2025-11-24}
2
+
\title{SAPLING Report}
3
+
\p{Today I went with many colleagues to [[google-syd]] for the [Sydney Area Programming Languages Interest Group (SAPLING) 2025 meeting](https://comp.anu.edu.au/sapling/index.html). I didn't present anything at the meeting but my PhD student, [[xinloi]] did a lightning talk introducing her work on incorrectness logic.}
4
+
\p{It was good to see many colleagues from [[unsw]] and catch up with some of my former students who were now working for Google.}
+34
trees/loc-002K.tree
+34
trees/loc-002K.tree
···
1
+
\date{2025-11-30}
2
+
\author{liamoc}
3
+
\import{table-macros}
4
+
\title{The ICEL Lord's Prayer is Terrible}
5
+
\p{One of my \em{many} bugbears with the Australian Anglican liturgy for the mass (based on \em{A Prayer Book for Australia}) is that they adopted the absolutely atrocious "modern" version of the Lord's Prayer from the Vatican's International Commission on English in the Liturgy some time during the 1970s:}
6
+
\quote{\poem{
7
+
\line{Our Father in Heaven,}
8
+
\line{Hallowed be your name,}
9
+
\line{Your kingdom come,}
10
+
\line{Your will be done on Earth as in Heaven,}
11
+
\line{Give us today our daily bread,}
12
+
\line{And forgive us our sins,}
13
+
\line{As we forgive those who sin against us,}
14
+
\line{Save us from the time of trial,}
15
+
\line{And deliver us from evil.}
16
+
\line{(For the Kingdom, the Power and the Glory are yours, now and forever.)}
17
+
\line{Amen}
18
+
}}
19
+
\p{I won't get into whether or why the doxology should or shouldn't be included in the prayer (although the answer is that it shouldn't), but I think this is an absolutely \em{terrible} translation that is so egregiously bad that I mumble the prayer in Latin at that point in the service at All Saints when I sing there.}
20
+
\p{About 50-60 years ago when the ICEL attempted to make modern translations of liturgical prayers, they had four main goals in mind:}
21
+
\ul{\li{\strong{Accessibility to normal English speakers}. Unlike the archaic BCP English which often tends to be poetic, the ICEL liturgy was intended to be straightforward for normal English speakers with no special training to understand.}
22
+
\li{\strong{Avoiding theological pitfalls}. Lines such as "Lead us not into temptation" should be avoided because they imply that God somehow directly tempts us, which is theologically problematic. }
23
+
\li{\strong{Ecumenism}. The liturgy was intended for Roman Catholic liturgies worldwide, across all English-speaking cultures, and the liturgical movement it started was also carried forward by many mainline Protestant and Anglican churches.}
24
+
\li{\strong{Dynamic Equivalence}. Avoiding direct translation from the Latin or Greek, but instead trying to convey meaning in a natural, idiomatic, modern way for the target language.}
25
+
}
26
+
\p{I personally disagree with some of these goals, but even putting aside my personal disagreements, I think this version of the prayer fails at all of these goals.}
27
+
\ul{\li{\strong{Accessibility to normal English speakers}. The line "Save us from the time of trial" seems to be referring to a particular time in the future — perhaps the time when Christ returns — rather than the trials and temptations of everyday life, to which the prayer was originally referring. In fact, I suspect almost all English-speaking Christians would think this line now refers to an apocalyptic time of trial. Doesn't seem very accessible to me.}
28
+
\li{\strong{Avoiding theological pitfalls}. They got rid of the theological problem of "leading into temptation" but added a brand new one: "As we forgive those who sin against us". Firstly, this line implies that it is possible to sin against a human being ("Every sin is chiefly against God" - Thomas Aquinas, ST-II-II 66.6) and, even worse, that human beings have the capacity to forgive sins ("Who can forgive sins but God alone?" - Mark 2:7). }
29
+
\li{\strong{Ecumenism}. The ICEL came up with this translation for use in Roman Catholic liturgy, but it has now been completely removed from use in the same liturgy (and even before, was usually only used in a few dioceses), replaced with a much more direct translation from the Latin Missal. In fact, the only churches still using this terrible translation are mostly Anglican churches like mine.}
30
+
\li{\strong{Dynamic Equivalence}. They half-assed this, replacing the "thy"s and "art"s but leaving in several turns of phrase that clearly come from the Book of Common Prayer ("Hallowed be your name") that don't sound natural or idiomatic in modern English. }
31
+
}
32
+
\p{I think there's some value in having something beautiful, poetic, or outside the norm in the liturgy. I think this is the value of the Latin liturgy, but the same value can be found in the poetic language of the BCP liturgies. Having something that appears "not of this world", different from the mundane language we use every day, is important to elevate the liturgy and set it apart from the normal day-to-day life of worshippers. The whole idea of "Dynamic Equivalence" robs the liturgy of its distinctiveness. I hope one day my church will put the APBA in the dustbin of history where it belongs.}
33
+
34
+
+13
trees/weeknotes/2025-W48.tree
+13
trees/weeknotes/2025-W48.tree
···
1
+
\import{table-macros}
2
+
\title{Weeknotes 2025-W48}
3
+
\author{liamoc}
4
+
\date{2025-11-30}
5
+
\p{I spent much of this week preparing notes for my upcoming Logic Summer School course, [[isa-0001]].}
6
+
\figure{
7
+
\<html:img>[width]{250px}[src]{\route-asset{assets/clear1.jpeg}}%{}
8
+
\<html:img>[width]{250px}[src]{\route-asset{assets/clear2.jpeg}}{}
9
+
\figcaption{Clear skies on my walk to work.}
10
+
}
11
+
\transclude{loc-002J}
12
+
\transclude{loc-002K}
13
+
\transclude{loc-002I}