@jfdm@discuss.systems

Jan de Muijnck-Hughes @jfdm@discuss.systems · Jul 27, 2026

Replying to @jfdm@discuss.systems

@agl@infosec.exchange I should add. I am not trying to dismiss you, I work in the area and there are lots of fascinating things here and good things too.

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Jul 27, 2026

Replying to @agl@infosec.exchange

@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.

1

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Jul 27, 2026

Replying to @agl@infosec.exchange

@agl@infosec.exchange To be frank, dependently-typed languages have always been interesting and we have had the machine help us write the code long before GenAI/LLMs became 'de jour'. The devil appears with writing your initial theorems not when asking the machines to provide proofs. The old mantra still exists: Garbage in; Garbage out. Bad propositions in; Bad proofs out.

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Jul 27, 2026

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.)

1

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Jul 24, 2026

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...

1

0

1

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Jul 14, 2026

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

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

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Jun 29, 2026

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

2

0

1

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Jun 28, 2026

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

0

1

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Jun 24, 2026

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.

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · May 18, 2026

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….

1

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · May 09, 2026

Replying to @jfdm@discuss.systems

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.

2

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · May 09, 2026

The rise of Reform is not too unexpected. Voters are disenfranchised, almost, like never before. If the ‘big parties’ cannot be trusted, or there is no confidence in them, who else are swing/unsure voters going to flock too! The smooth talking snake oil sales party.

I honestly do not think Labour should get rid of Sir Kier. I think the UK labour government are, on the whole, doing good things at the UK/England level. I think their PR team are not doing their job properly. I think this is Sir Keir’s problem, he’s a politician’s politician but his optics are not great. Fix the optics and things should be better.

In Scotland, on the otherhand, I have not liked the pamphlets coming through the door. For many, that is your first contact with a party. Just saying that SNP is bad is not good enough. You need to say more on what you will do.

As for Wales…

2

4

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · May 08, 2026

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
```

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · May 08, 2026

Replying to @jfdm@discuss.systems

@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....

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · May 08, 2026

Replying to @gallais@mamot.fr

@gallais@mamot.fr I’ve so far resisted getting the spreadsheet out…

0

1

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · May 08, 2026

Replying to @jfdm@discuss.systems

Although cannot wait to see how the seats could have looked like had a purely PR system been used… Question is, why does one use as input data?

0

4

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · May 08, 2026

Is it safe to come out now! #ukpol #scotpol #cymrupoli that light blue is scary

discuss.systems

0

5

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · May 06, 2026

Replying to @bjacobs@social.edu.nl

@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.

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · May 06, 2026

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"

3

0

1

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Apr 22, 2026

Replying to @jfdm@discuss.systems

I should write a python tool to do this, it is basic data science and no idea why we cannot have a drill to do this. It is not as if we do it multiple times per year, every year.... oh wait...

1

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Apr 22, 2026

As a user I want my big drill to automatically generate certain plots about my data, and statistics so I can package to a local drill in xlsx format...

Big Drill: only histograms and some statistics..

Me: Throws big drill in the bin.

Me: Turns to Locally Made drill, can I give you the data, and you can give me plots and statistics.

Locally Made drill: for some of your final data yes and not to you but your boss can get it later and they can share it with you...

Me: Throws locally made drill in the bin

Me: Turns to Office365 drill, can you do this for me;

Office365 Drill: yes but it will cost you...

Me sighs, cuts finger, draws pentagon and sigils, and chants...

2

1

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Apr 21, 2026

Replying to @lindsey@recurse.social

@lindsey great colleagues of mine do this, and even have a competition for best drawing…

0

1

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Apr 20, 2026

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…

2

1

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Apr 19, 2026

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….

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Apr 16, 2026

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

6

1

3

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Apr 15, 2026

Replying to @bodzioney@mathstodon.xyz

@bodzioney putting it mildly we are a home of many cool pl communities, and if pl itself. Seriously there are always more academics than people think at university’s and should use guides like these as a stepping stone to who else is there! Sadly funding will be an issue in the UK at least….

2

1

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Apr 15, 2026

Replying to @bodzioney@mathstodon.xyz

@bodzioney https://spli.scot/supervisors.html there are dozens of us!

1

3

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Apr 14, 2026

Replying to @okennedy@discuss.systems

@okennedy @liamoc @gallais after speaking to some peers, I’m highly tempted to have ‘class tests’ replace the summative coursework. Only way to ensure no gen ai. Cannot do as fancy, or same indepth work, but it’s a trade off I’m willing to think about to ensure students are tested on fundamentals.

2

1

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Apr 14, 2026

Replying to @gallais@mamot.fr

@gallais very true, I was thinking of check-ins, reflective journals, and trusted git history….

0

5

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Apr 14, 2026

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)

2

7

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Apr 13, 2026

Replying to @jfdm@discuss.systems

@gallais urgh ‘s/lookup/loomio/‘

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Apr 13, 2026

Replying to @gallais@mamot.fr

@gallais I imagine so, I’m still partial to the idea of more structured asynchronous decisions processes (e.g. lookup) as they can make all voices heard fairly and not just the loud opinionated professors.

1

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Apr 10, 2026

Replying to @jfdm@discuss.systems

Qapla' ! Custom Git log formats, Markdown, Pandoc are your friends: ``` git log --patch --pretty=format:"\`\`\`%n%n# Commit %h %s%n%n+ Author :: %an%n+ Email :: %ae%n+ Date :: %ad%n+ Long Commit :: %H%n%n Commit Mesage%n%n\`\`\`%n%s%n%b\`\`\`%n%n Code Difference%n\`\`\`%n" \ | sed '1d' \ | sed '$a```\n' \ | pandoc --from=markdown --to=html5 --table-of-contents --standalone \ --metadata=title:"Git Log for " > ï½¿ -logs.html ``` where `` is the students registration number, and `` are paths to files I am interested in. Caveats: + log format is *just* for logs, so too is `--output`. So if you want to include code changes then you need to capture `stdout`; + capturing patches means you need to have a leading end delimiter and a trailing start deliminter; + `sed` magic removes the first leading end delimiter, and inserts a final end delimiter; + markdown/commonmark to insert raw html for foldable summaries of commit message and code diff + pandoc to get standalone html files and tocs

0

1

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Apr 09, 2026

Dos anyone know if there are good utilities to generate a static interactive html pages for #git log files. Need to submit evidence to those not tech savvy.

1

4

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Mar 29, 2026

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…

2

0

1

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Mar 25, 2026

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…

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Mar 21, 2026

Replying to @edwinb@types.pl

@edwinb good luck with the curriculum discussions! The dicussons are actually interesting as it forces us to think outside our comfort areas. CS is a cyber-physical socio-technical theory and practice based subject. At St Andrews it’s compounded with the major minor tertiary module structure. You need the polder model if discussions are going to work. Related side note, I remember years ago hearing a discussion in St Andrews about first languages. Fascinating the arguments were.

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Mar 20, 2026

Replying to @jfdm@discuss.systems

At least everything else appears to be working and I have freed up a bit more space….

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Mar 20, 2026

Replying to @jfdm@discuss.systems

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...

0

1

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Mar 20, 2026

lets do `nix-channel --update` and see if everything still works....

1

2

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Mar 20, 2026

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...

2

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Mar 16, 2026

Replying to @jer_gib@functional.cafe

@jer_gib UK HEI HR Systems!

1

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Mar 16, 2026

Oracle Databases 0; /me 2

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

2

1

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Mar 07, 2026

Replying to @jschuster@hachyderm.io

@jschuster @shriramk @cross @lindsey @krismicinski@types.pl @csgordon @jeremysiek well that’s what I’m hoping to help chip away at.

2

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Mar 07, 2026

Replying to @jschuster@hachyderm.io

@jschuster @shriramk @cross @lindsey @krismicinski@types.pl @csgordon @jeremysiek well some of us like behavioural (& other substructures) types and acvitivity and interaction diagrams (really models) provide a nice end user view of what the types should look like.

1

2

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Mar 05, 2026

Replying to @jeremysiek@types.pl

@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,

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.
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.

2

1

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Mar 05, 2026

Replying to @csgordon@discuss.systems

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

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

Either way, we are doomed.

3

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Mar 05, 2026

Replying to @csgordon@discuss.systems

@csgordon@discuss.systems @lindsey@recurse.social @jeremysiek@types.pl @krismicinski@types.pl I know it doesn’t help much, but I ask my students to produce a short report along side the technical submission. The idea being you can eyeball the differences between written report and code submission. Identify where more interrogation isrequired. I know genai could produce these reports but every little helps. Submission canaries, for want of a better phrase.

4

3

1

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Dec 18, 2025

Replying to @xot@someone.elses.computer

@xot@someone.elses.computer Regardless, there has been some movement overnight: See towards the end of this thread: https://infosec.exchange/@hovav/115731038692335809 Regardless, I still think an openletter.earth petition would send a good message. Apparently, the setup was ignoring CC-BY-*ND*!

0

Jan de Muijnck-Hughes @jfdm@discuss.systems · Dec 17, 2025

Replying to @jesper@agda.club

@jesper@agda.club @peter_sewell_@types.pl @wilbowma@types.pl IIRC @xot@someone.elses.computer had some nice infrastructure for getting open letters signed. Perhaps he can chime in...

1

0

Jan de Muijnck-Hughes

Posts

discuss.systems

Remote instance