my forest
weeknotes week 30
+85
-1
+1
trees/loc-001B.tree
+1
trees/loc-001B.tree
+10
trees/loc-001I.tree
+10
trees/loc-001I.tree
···
1
+
\date{2025-07-27T10:13:22Z}
2
+
\author{liamoc}
3
+
\title{Engagement Crisis in Teaching}
4
+
\p{While this is my time convening [a first year computing course](COMP1100), I have taught lectures for first year before, and I have convened [large courses](COMP3141) before. I consider myself a fairly experienced lecturer. Yet, I was both shocked and deeply troubled to see that, of the 120-odd students that enrolled in my first year computing course (this is the "off-session" run of the very first introductory computing course), only about 40 or so attended the first lecture and, even optimistically assuming that there is no overlap between online viewers and in-person viewers, only about 40 further students saw the lectures online. This means I only saw about a third of the course in person, and a third haven't even participated in lectures remotely, let alone in person. }
5
+
\p{I think this is an enormous shame. Learning stuff is only part of the reason to attend university. Far more important, at least in my view, is the social aspect. It is one of the few times in an adult's life where it's basically okay to sit next to someone you don't know and just talk to them. After leaving university, the social opportunities can easily dry up, and it pains me to see students basically intentionally throwing this away in favour of online learning.}
6
+
\p{If I compare to the very first university lecture I ever attended, back in 2008 at [[unsw]], which is [still on YouTube for easy comparison](https://www.youtube.com/watch?v=hE7l6Adoiiw), it's easy to tell even from the video that the lecture theatre was nearly packed, and the energy among students is high.}
7
+
\p{Now, I'm not as charismatic or engaging as Richard Buckland, but my students this year are not even \em{giving me a chance to bore them}. They didn't attend from the \em{very first lecture}. It's quite demoralising. }
8
+
\p{I also noticed that, of the students that thankfully did attend, at first getting them to engage with even simple questions was very challenging. Partly this was because of the configuration of the room (once I realised how to turn on the front lights after turning on the projector auto-dimmed them, engagement improved), and partly it might have been just some initial nerves from the students. I think the situation is improving with regards to in-person engagement, but attendance is still shockingly low.}
9
+
\p{My colleagues tell me that attendance figures have been similarly bad ever since COVID hit. Because the course I taught at the [[uoe]] was [an optional later-year elective](itcs), I never really observed this problem at UoE, although it could well have been there. I'm curious as to other universities' experience of this. Have there been any techniques that students both \em{liked} and which motivated them to attend in person? }
10
+
\p{I have talked to some colleagues for advice on how to address this, and I got suggestions from withholding marks to bribery, but I think all I can do is teach the people that actually show up to my class, and ignore those that don't. It's quite a dispiriting state of affairs, though.}
+58
trees/loc-001J.tree
+58
trees/loc-001J.tree
···
1
+
\import{table-macros}
2
+
\def\percent{\startverb%\stopverb
3
+
}
4
+
\parent{loc-000P}
5
+
\title{7th Sunday After Pentecost 2025}
6
+
\tag{cmc}
7
+
\date{2025-07-27}
8
+
\author{liamoc}
9
+
\quote{
10
+
Deus in loco sancto suo: Deus, qui inhabitáre facit unánimes in domo: ipse dabit virtútem et fortitúdinem plebi suæ.
11
+
}
12
+
\p{Today our choir at [All Saints Ainslie](https://allsaintsainslie.org.au) performed Batten's anthem [O Sing Joyfully](https://www.youtube.com/watch?v=-gHkKGiXeNE):}
13
+
\quote{
14
+
\poem{
15
+
\line{O sing joyfully, O sing joyfully unto God our strength;}
16
+
\line{Make a cheerful noise unto the God of Jacob.}
17
+
\line{Take the song, bring hither the tabret:}
18
+
\line{The merry harp with the lute! Blow up!}
19
+
\line{Blow up the trumpet in the new moon:}
20
+
\line{Ev'n in the time appointed and upon our solemn feast day.}
21
+
\line{For this was made a statute for Israel}
22
+
\line{And a law of the God of Jacob.}
23
+
}
24
+
}
25
+
\p{It was also the three years mind of the philosopher Geoffrey Brennan, the late husband of Margaret, a soprano in our choir. Perhaps by coincidence or perhaps because our director Alasdair chose it intentionally (I'm not sure which), we sang the appropriate hymn [Be Still, My Soul](https://www.youtube.com/watch?v=QYbX9wmQTlI) which always brings a tear to my eye. It was also a hymn I selected for the funeral of my grandfather. I don't normally post the hymn lyrics here, but I'll make an exception in this case. }
26
+
\quote{
27
+
\poem{
28
+
\line{Be still, my soul! The Lord is on your side;}
29
+
\line{Bear patiently the cross of grief or pain;}
30
+
\line{Leave to your God to order and provide;}
31
+
\line{In ev'ry change he faithful will remain.}
32
+
\line{Be still, my soul! Your best, your heav’nly friend}
33
+
\line{Thru' thorny ways leads to a joyful end.}
34
+
\line{\br}
35
+
\line{Be still, my soul! Your God does undertake}
36
+
\line{To guide the future as he has the past;}
37
+
\line{Your hope, your confidence, let nothing shake;}
38
+
\line{All now mysterious shall be bright at last.}
39
+
\line{Be still, my soul! the waves and winds still know}
40
+
\line{His voice who ruled them while he lived below. }
41
+
\line{\br}
42
+
\line{Be still, my soul! When dearest friends depart}
43
+
\line{And all is darkened in the vale of tears,}
44
+
\line{Then shall you better know his love, his heart,}
45
+
\line{Who comes to soothe your sorrow and your fears.}
46
+
\line{Be still, my soul! Your Jesus can repay}
47
+
\line{From his own fullness all he takes away.}
48
+
\line{\br}
49
+
\line{Be still, my soul! The hour is hast'ning on}
50
+
\line{When we shall be forever with the Lord,}
51
+
\line{When disappointment, grief, and fear are gone,}
52
+
\line{Sorrow forgot, love's purest joys restored.}
53
+
\line{Be still my soul! When change and tears are past,}
54
+
\line{All safe and blessed we shall meet at last.}
55
+
}
56
+
}
57
+
58
+
\p{I didn't go to Evensong today because it was raining quite badly and I had to prepare my lectures.}
-1
trees/refs/linares-dajosr-2025.tree
-1
trees/refs/linares-dajosr-2025.tree
···
11
11
%\meta{doi}{}
12
12
\tag{cogent}
13
13
\tag{refereed}
14
-
\p{This paper is the fulfillment of the research I envisioned in [my paper at VIMPL of a similar name](oconnor-linares-rizkallah-2023).}
15
14
\p{Programming languages with uniqueness type systems prevent pointer aliasing, simplifying memory safety reasoning. However, code implemented in these languages often interoperates through foreign function interfaces with external components implemented in languages lacking the same level of static safety guarantees. To verify safe updates in a combined system, one must manually verify that the external components preserve the safety invariants of the uniqueness type system. In particular, recent work showed that one can manually discharge such obligations on C components from a cross-language Cogent-C system by directly reasoning about the C code in higher-order logic. However, even for simple examples, discharging the uniqueness safety obligations, known as frame conditions, within a logic not specifically designed for direct reasoning in terms of heaps and pointers was not ideal. Separation logic is an established logic that facilitates reasoning about imperative programs by localising reasoning to the parts of the heap that the program mutates. This raises a vital question. Can we use separation logic to discharge the safety obligations imposed by uniqueness types? The answer is yes. This paper demonstrates that the frame conditions can be inferred from particular separation logic triples and, hence, discharged by reasoning using separation logic. We identify and verify the soundness of specific separation logic triples that imply the frame conditions imposed by a uniqueness type system.}
16
15
17
16
\p{To appear.}
+16
trees/weeknotes/2025-W30.tree
+16
trees/weeknotes/2025-W30.tree
···
1
+
\title{Weeknotes 2025-W30}
2
+
\author{liamoc}
3
+
\date{2025-07-27}
4
+
\p{I started teaching the course [[COMP1100]] this week. I also got some good news: [[selene]] and several other authors (including me) recently got news that our paper was accepted to [APLAS '25](aplas25). }
5
+
\transclude{loc-001I}
6
+
\subtree{
7
+
\author{liamoc}
8
+
\title{Paper publication success at APLAS}
9
+
\p{This paper is the fulfillment of the research I envisioned in [my paper at VIMPL of a similar name](oconnor-linares-rizkallah-2023).}
10
+
\p{Since then, [Selene](selene) has worked to actually formalise and figure out what are, in my paper, just the vaguest of intuitions. It's nice to see this come together!}
11
+
\scope{
12
+
\put\transclude/metadata{true}
13
+
\transclude{linares-dajosr-2025}
14
+
}
15
+
}
16
+
\transclude{loc-001J}