Jan de Muijnck-Hughes

Back to books - Sweden's schools give up digital learning https://www.bbc.co.uk/news/articles/cly0vk77vdko

a cut finger makes typing harder a while....

@agl@infosec.exchange

I think we haven’t really explored this in normal contexts.

Indeed, there are actually "dozens" of us who want to, and are exploring, how to bring this interesting paradigm to others. As well as exploring what this paradigm gives us in the first place..

I feel that the overhead of these languages previously precluded their use in all but specialised domains. Now that the overhead is much less, I think it’s an interesting avenue to explore. But certainly not a guaranteed success.

Indeed!

If you are not familiar with it already, you should explore:

https://hacspec.org/

It shows one way of doing things.

There are, however, other dependently typed languages (Agda/Idris2) which provide a different view (compared to Roq/Lean) of working with the machine to build verified software.

Eek a week till SPLV, and it might be time to start thinking about what I want to do for my three hours ;-)

(Hint: I already have, but I am battling the procrastination monster.)

As much as I like the GIFT format, as mustered by Moodle, it does not capture the nearly as much of the metadata as the XML format.

For essay questions I want to specify the maximum grade directly within the file itself, and not later on the VLE...

Work > "Hi everyone here are key dates for your calendar";

Me > "Great, will be good to add them to my calendar. Where is the iCal URL so I can import your calendar into mine..."

Work > "Sharepoint lets you download each event as an individual iCal file. How great is that!"

Me > "But there are like more than 30 events I want to add..."

Work > "Sharepoint lets us have a single University wide 'events page' that you can filter through"

Me > "But I want to add to my own calendar or subscribe to an iCal you produce!"

Work > "Sharepoint lets us have a single University wide 'events page' that you can filter through"

Me > "Urgh, I will stick with Org Mode and generate the iCal from there"

Urgh,

only independence will enable us to tackle reform….

What a load of bollocks! As always SNP are shifting the blame to Westminster. Reform is a UK problem, and Reform are now entrenched in all levels of British politics. Ireland have their own loonies. Sadly reform are legitimate because of the electorate. So no treating them like a joke, we must dismantle them by showing that their policies and ideas are not what are needed. Help the electorate understand why your actions are best.

Scotland used to take pride in the ‘high-level of debate’ around the time of IndyRef in 2015. Bring that same level back to how politics is discussed.

That feeling when you realise you may have left your nice travel cutlery in the public work kitchenette.

I’ve not been in for a few days. Fingers crossed it is still there…I cannot find them anywhere at home…

@csgordon@discuss.systems @lindsey@recurse.social @jeremysiek@types.pl @krismicinski@types.pl There are two routes I have considered:

1. learn how to write more open book take home assignments;
2. get students to do programming coursework in the lab in exam conditions

Either way, we are doomed.

Current thoughts: assessment design so that students authentically document their thought-process more than their outputs.

GenAI is hurting those that attempt assessment of fundamental concepts authentically (without using GenAI) and those that lean on GenAI to get a mark.

(This whole thing makes me sad for my students)

I gave a research lecture to students today at #TypeSig #Triple. #UoE The topic was that of my #TYPES2025 talk: Being Positively Negative About Dependent Types.

Great range of speakers from organisers, even though it was @mspstrath@mastodon.acm.org heavy! One student came at the end to say they enjoyed the talk as it was accessible to them. I like that.

Also nice to see the other talks in the tracks I attended. Especially those that are related! (Two sided type systems)

The journey home even gave me space to think about research…

I wish #Moodle email notifications for activities included the module code or title by-default in the subject.

Receiving multiple notifications for 'Coursework 1', can be confusing.

Even module notices do not include the module code/title in the subject. I have to include the code by hand...

Oracle Databases 0; /me 2

That is two Universities that, for some reason, have core systems that do not like my surname....

Mmhh thought about suggesting a `MSP.sty` for common macros for PLT related LaTeX shenanigans.

More chance of the local football team’s supporters burying the hatchet and being nice to each other….

@shriramk@mastodon.social @csgordon@discuss.systems @lindsey@recurse.social @jeremysiek@types.pl @krismicinski@types.pl right so to be clear on these things, the doom part is because the actions require not so trivial changes in how we do things. Within UK academia we are under lots of pressures, with not a lot of time, and not the same power and influence as 'full chairs' do in the states.

More so,

1. open book assignments do not exclude the use of GenAI, they can embrace it, and you can guard against or incorporate its use. Such assignments, in my experience are harder to design, and require training on how to do well.

2. Exam conditions are also important as we want students to not rely on GenAI, and to ensure they have the fundamentals down.

The argument with GenAI is must be how our forefathers thought about pocket calculators...and their forefathers thought about slide rules, and so on.

aujourd'hui les musique c'etait musique électronique de AIR et Daft Punk.

How did these two duo's not collaborate...

Using D'Hondt sans regions for Wales:

```
- PC: 36 seats
- REF: 29 seats
- LAB: 11 seats
- CON: 10 seats
- GREEN: 6 seats
- LBD: 4 seats
```

Urgh. Why on earth do you want a battery powered system for a bin to make it ‘no touch’.

Pedal bins are just as good and repairable.

Shame though, it’s a nice looking bin….

@bjacobs BTW, if you change your LaTeX preamble to include the following:

\usepackage{xcolor}
\definecolor{impactRed}{RGB/cymk}{227,0,11/0,100,100,0} 
\usecolortheme[named=impactRed]{structure}

the purple coloured list labels (and text) should be replaced with labels and text in the official 'Impact RED' of the RU branding.

urgh, I wish our moodle had an explicit exam activity for managing exam returns. Not that I enjoy moodle, but I want to reduce how many duplicate shadow systems I need to maintain and still teach the way I want to teach... the issue being how to aggregate questions as sometimes having attempt n out of m questions is a nic,e format.

From the other site, but too good to not share:

https://x.com/robertgraham/status/2036208633814639088

There is a post about the importance of the BBC’s ‘pips’ arising form commenting on someone demonstrating a plugin that plays the BBC news countdown (that includes the ‘pips’) as the countdown to a teams meeting. I wish I could get this before all meetings I have to attend…

well...

• had to install new nix
• first I ran out of diskspace...
• nix-env to delete old generations
• commented out most of home.nix
• nix-collect-garbage
• nix-store --optimise
• watched my diskspace go up and down like a yoyo

Now nix commands do not have man pages...

@gallais@mamot.fr

Right with a D'Hondt calculation (from the Internet) I got:

D'Hondt Seat Allocation:
- SNP: 37 seats
- LAB: 22 seats
- REF: 22 seats
- SGP: 19 seats
- CON: 16 seats
- LDM: 11 seats
- ALS: 1 seats
- SCP: 0 seats
- WPB: 0 seats
- ADF: 0 seats
- EELP: 0 seats
- ASP: 0 seats
- ADVUK: 0 seats
- SLP: 0 seats
- AWP: 0 seats
- CPB: 0 seats

so pretty close-ish....

@gallais@piaille.fr apparently aldi’s ice cream is made by mackie.