Elektrine
EN
Log in Register
Paige Chat Timeline Communities Gallery Videos Email DNS VPN Uptime Kairo
Back to Timeline
Remote

James Wood

@mudri@mathstodon.xyz
mastodon 4.6.4
  • Open on mathstodon.xyz

(2025-06-24) Programming Languages at Huawei. Formerly, linear and modal type systems in Agda. Thesis: https://stax.strath.ac.uk/concern/theses/tt44pn44w. Website: https://lamudri.github.io/.

0 Followers
0 Following
22 Posts
Joined October 29, 2022

Posts

Open post
mudri
James Wood @mudri@mathstodon.xyz · May 14, 2026
James Wood
@mudri@mathstodon.xyz

(2025-06-24) Programming Languages at Huawei. Formerly, linear and modal type systems in Agda. Thesis: https://stax.strath.ac.uk/concern/theses/tt44pn44w. Website: https://lamudri.github.io/.

mathstodon.xyz

A 35 to Easter Road, taken from a 35 to Ocean Terminal.

0
1
0
0
Open post
mudri
James Wood @mudri@mathstodon.xyz · May 11, 2026
James Wood
@mudri@mathstodon.xyz

(2025-06-24) Programming Languages at Huawei. Formerly, linear and modal type systems in Agda. Thesis: https://stax.strath.ac.uk/concern/theses/tt44pn44w. Website: https://lamudri.github.io/.

mathstodon.xyz
Replying to @jonmsterling@mathstodon.xyz
@jonmsterling@mathstodon.xyz In a slightly different area, I bet some people are already nostalgic for the days when you could look things up on Wikipedia and get reliable information without feeling guilty about using so much electricity and water.
1
0
0
0
Open post
mudri
James Wood @mudri@mathstodon.xyz · May 09, 2026
James Wood
@mudri@mathstodon.xyz

(2025-06-24) Programming Languages at Huawei. Formerly, linear and modal type systems in Agda. Thesis: https://stax.strath.ac.uk/concern/theses/tt44pn44w. Website: https://lamudri.github.io/.

mathstodon.xyz
Replying to @jfdm@discuss.systems
@jfdm@discuss.systems The only plan I noticed being articulated this Scottish Parliament campaign was the SNP's plan to ask for another independence referendum.
0
0
0
0
Open post
mudri
James Wood @mudri@mathstodon.xyz · May 06, 2026
James Wood
@mudri@mathstodon.xyz

(2025-06-24) Programming Languages at Huawei. Formerly, linear and modal type systems in Agda. Thesis: https://stax.strath.ac.uk/concern/theses/tt44pn44w. Website: https://lamudri.github.io/.

mathstodon.xyz
Replying to @julesh@mathstodon.xyz
@julesh@mathstodon.xyz ⋃𝒫X = X.
1
0
0
0
Open post
mudri
James Wood @mudri@mathstodon.xyz · May 06, 2026
James Wood
@mudri@mathstodon.xyz

(2025-06-24) Programming Languages at Huawei. Formerly, linear and modal type systems in Agda. Thesis: https://stax.strath.ac.uk/concern/theses/tt44pn44w. Website: https://lamudri.github.io/.

mathstodon.xyz
Replying to @anuytstt@fosstodon.org
@anuytstt@fosstodon.org @tubemapper@mastodonapp.uk And Greater Anglia trains are, in turn, aped from them?
1
0
0
0
Open post
mudri
James Wood @mudri@mathstodon.xyz · May 03, 2026
James Wood
@mudri@mathstodon.xyz

(2025-06-24) Programming Languages at Huawei. Formerly, linear and modal type systems in Agda. Thesis: https://stax.strath.ac.uk/concern/theses/tt44pn44w. Website: https://lamudri.github.io/.

mathstodon.xyz
Replying to @joomy@functional.cafe
@joomy@functional.cafe Yeah, I don't know what sort of tricks the best-performing engines use, but I was surprised how badly fairly naïve search performed when I implemented it. The one on my phone can exactly solve 20-ply endgames almost instantly, while I was struggling with 8 IIRC.
0
0
0
0
Open post
mudri
James Wood @mudri@mathstodon.xyz · May 03, 2026
James Wood
@mudri@mathstodon.xyz

(2025-06-24) Programming Languages at Huawei. Formerly, linear and modal type systems in Agda. Thesis: https://stax.strath.ac.uk/concern/theses/tt44pn44w. Website: https://lamudri.github.io/.

mathstodon.xyz
Replying to @joomy@functional.cafe
@joomy@functional.cafe For what it's worth, I just spent a few hours playing a game against Reversirocq on master difficulty and won fairly comfortably.
0
3
0
0
Open post
mudri
James Wood @mudri@mathstodon.xyz · Apr 23, 2026
James Wood
@mudri@mathstodon.xyz

(2025-06-24) Programming Languages at Huawei. Formerly, linear and modal type systems in Agda. Thesis: https://stax.strath.ac.uk/concern/theses/tt44pn44w. Website: https://lamudri.github.io/.

mathstodon.xyz

Wow, there's an incredible temperature difference between Edinburgh and Glasgow at the moment. Glasgow has had a basically warm day and evening, while Edinburgh is getting a frost.

For context, these places are 67 km (42 mi) east-west of each other.

1
0
0
0
Open post
mudri
James Wood @mudri@mathstodon.xyz · Apr 21, 2026
James Wood
@mudri@mathstodon.xyz

(2025-06-24) Programming Languages at Huawei. Formerly, linear and modal type systems in Agda. Thesis: https://stax.strath.ac.uk/concern/theses/tt44pn44w. Website: https://lamudri.github.io/.

mathstodon.xyz

What I hate most about going to the dentist's is the misaligned incentives. Well, that and the gum-stabbing.

3
1
0
0
Open post
mudri
James Wood @mudri@mathstodon.xyz · Apr 14, 2026
James Wood
@mudri@mathstodon.xyz

(2025-06-24) Programming Languages at Huawei. Formerly, linear and modal type systems in Agda. Thesis: https://stax.strath.ac.uk/concern/theses/tt44pn44w. Website: https://lamudri.github.io/.

mathstodon.xyz
Replying to @joomy@functional.cafe
@joomy@functional.cafe I'll have to give it a go when I get the chance, to see how it plays.
1
0
0
0
Open post
mudri
James Wood @mudri@mathstodon.xyz · Apr 14, 2026
James Wood
@mudri@mathstodon.xyz

(2025-06-24) Programming Languages at Huawei. Formerly, linear and modal type systems in Agda. Thesis: https://stax.strath.ac.uk/concern/theses/tt44pn44w. Website: https://lamudri.github.io/.

mathstodon.xyz
Replying to @joomy@functional.cafe
@joomy@functional.cafe Nice project! What's the heuristic when you reach the search depth limit?
0
2
0
0
Open post
mudri
James Wood @mudri@mathstodon.xyz · Apr 02, 2026
James Wood
@mudri@mathstodon.xyz

(2025-06-24) Programming Languages at Huawei. Formerly, linear and modal type systems in Agda. Thesis: https://stax.strath.ac.uk/concern/theses/tt44pn44w. Website: https://lamudri.github.io/.

mathstodon.xyz
Replying to @craigfrancis@mastodon.social
@craigfrancis@mastodon.social As far as I'm aware, there is indeed nothing like this. We could consider adding it, though, if the case is strong enough. My instinct would be for library APIs to deal entirely in ASTs, and never parse strings at runtime. C#'s LINQ seems to show that this is possible (even without the fancy SQL-like syntax sugar, the query builder methods seem quite serviceable and expressive). Are there problems with this, either security-wise or practically?
1
2
0
0
Open post
mudri
James Wood @mudri@mathstodon.xyz · Apr 01, 2026
James Wood
@mudri@mathstodon.xyz

(2025-06-24) Programming Languages at Huawei. Formerly, linear and modal type systems in Agda. Thesis: https://stax.strath.ac.uk/concern/theses/tt44pn44w. Website: https://lamudri.github.io/.

mathstodon.xyz
Replying to @mudri@mathstodon.xyz
We also have a Discord guild for Cangjie, where not much is happening at the moment, but most of the Edinburgh team are ready to be prodded about features or design decisions or getting stuff to run or whatever: https://discord.gg/bCzzaujKUv
1
0
0
0
Open post
mudri
James Wood @mudri@mathstodon.xyz · Apr 01, 2026
James Wood
@mudri@mathstodon.xyz

(2025-06-24) Programming Languages at Huawei. Formerly, linear and modal type systems in Agda. Thesis: https://stax.strath.ac.uk/concern/theses/tt44pn44w. Website: https://lamudri.github.io/.

mathstodon.xyz
Replying to @mudri@mathstodon.xyz
(Not an April fool's joke!)
0
1
0
0
Open post
mudri
James Wood @mudri@mathstodon.xyz · Apr 01, 2026
James Wood
@mudri@mathstodon.xyz

(2025-06-24) Programming Languages at Huawei. Formerly, linear and modal type systems in Agda. Thesis: https://stax.strath.ac.uk/concern/theses/tt44pn44w. Website: https://lamudri.github.io/.

mathstodon.xyz

Overview of Cangjie Programming Language
https://jcst.ict.ac.cn/fileup/1000-9000/PDF/JCST-2603-OF-2509-15978.pdf

In case anyone's been wondering about the project I'm part of in Huawei, we have a paper out going through the language design and compiler architecture of Cangjie, linked above. Also everything is open source now, and available at https://gitcode.com/Cangjie/.

8
7
5
0
Open post
mudri
James Wood @mudri@mathstodon.xyz · Feb 27, 2026
James Wood
@mudri@mathstodon.xyz

(2025-06-24) Programming Languages at Huawei. Formerly, linear and modal type systems in Agda. Thesis: https://stax.strath.ac.uk/concern/theses/tt44pn44w. Website: https://lamudri.github.io/.

mathstodon.xyz
Replying to @calcifer@masto.hackers.town
@calcifer@masto.hackers.town @lmorchard@masto.hackers.town What is parroting patterns if not inducing a pattern and then applying that pattern to new inputs?
0
1
0
0
Open post
mudri
James Wood @mudri@mathstodon.xyz · Feb 27, 2026
James Wood
@mudri@mathstodon.xyz

(2025-06-24) Programming Languages at Huawei. Formerly, linear and modal type systems in Agda. Thesis: https://stax.strath.ac.uk/concern/theses/tt44pn44w. Website: https://lamudri.github.io/.

mathstodon.xyz
Replying to @hypolite@friendica.mrpetovan.com
@hypolite @lmorchard@masto.hackers.town Did you read the OP? It says “the answer is just repeating the most probable word combinations from its training dataset.”. The answer it gave me is not a probable word combination from the training dataset because it doesn't appear in the training dataset.
0
0
0
0
Open post
mudri
James Wood @mudri@mathstodon.xyz · Feb 26, 2026
James Wood
@mudri@mathstodon.xyz

(2025-06-24) Programming Languages at Huawei. Formerly, linear and modal type systems in Agda. Thesis: https://stax.strath.ac.uk/concern/theses/tt44pn44w. Website: https://lamudri.github.io/.

mathstodon.xyz
Replying to @lmorchard@masto.hackers.town
@lmorchard The ability to induce such a rule goes well beyond the OP's characterisation of what LLMs do.
0
2
0
0
Open post
mudri
James Wood @mudri@mathstodon.xyz · Feb 26, 2026
James Wood
@mudri@mathstodon.xyz

(2025-06-24) Programming Languages at Huawei. Formerly, linear and modal type systems in Agda. Thesis: https://stax.strath.ac.uk/concern/theses/tt44pn44w. Website: https://lamudri.github.io/.

mathstodon.xyz
Replying to @leeloo@chaosfem.tw

@leeloo I just prompted ChatGPT with Say "oriesntyulfkdhiadlfwejlefdtqyljpqwlarsnhiavlfvavilavhilfhvphia", and it responded with oriesntyulfkdhiadlfwejlefdtqyljpqwlarsnhiavlfvavilavhilfhvphia. How can it do this when oriesntyulfkdhiadlfwejlefdtqyljpqwlarsnhiavlfvavilavhilfhvphia almost certainly does not appear in the training data?

0
2
0
0
Open post
mudri
James Wood @mudri@mathstodon.xyz · Dec 29, 2025
James Wood
@mudri@mathstodon.xyz

(2025-06-24) Programming Languages at Huawei. Formerly, linear and modal type systems in Agda. Thesis: https://stax.strath.ac.uk/concern/theses/tt44pn44w. Website: https://lamudri.github.io/.

mathstodon.xyz
Replying to @glocq@mathstodon.xyz
@glocq@mathstodon.xyz @mcc@mastodon.social I'm pretty sure that song is why I know of Barbra Streisand, and I'm only 30.
2
2
0
0
Open post
mudri
James Wood @mudri@mathstodon.xyz · Dec 23, 2025
James Wood
@mudri@mathstodon.xyz

(2025-06-24) Programming Languages at Huawei. Formerly, linear and modal type systems in Agda. Thesis: https://stax.strath.ac.uk/concern/theses/tt44pn44w. Website: https://lamudri.github.io/.

mathstodon.xyz
Replying to @timnitGebru@dair-community.social
@timnitGebru@dair-community.social An observation: People in the Othello community (and I'm sure that of many other abstract strategy games) regularly refer to brute-force endgame evaluation as “AI”, even though it's just a naïve exhaustive search of the game tree. I think it's basically because it has the same interface as heuristic evaluation.
1
0
0
0
Open post
mudri
James Wood @mudri@mathstodon.xyz · Nov 06, 2022
James Wood
@mudri@mathstodon.xyz

(2025-06-24) Programming Languages at Huawei. Formerly, linear and modal type systems in Agda. Thesis: https://stax.strath.ac.uk/concern/theses/tt44pn44w. Website: https://lamudri.github.io/.

mathstodon.xyz
Replying to @johnwallace@mastodon.ie
@johnwallace@mastodon.ie @jerrylevine@mastodon.social People using Home rather than Latest Tweets see all sorts of rubbish thanks to likes and replies. The Mastodon behaviour is basically the same as Latest Tweets, as far as I can tell, except that you know that everyone else will be using it too.
2
1
1
0

Remote instance

mathstodon.xyz
Open on original server

Media

313k7r1n3
Elektrine

Tor hidden service

elekhj7afj4qnrr4yd3bkzslsyo5jgfxw3orgjkhlcxifueodybyiiad.onion

Platform

  • Email
  • Chat
  • Timeline
  • Communities
  • VPN
  • DNS

Company

  • About
  • Contact
  • FAQ

Legal

  • Terms of Service
  • Privacy Policy
  • Warrant Canary
  • Lite (no JS)
  • VPN Policy
  • Source code

Support

  • support@elektrine.com
  • Report Security Issue
Mail client setup IMAP mail.elektrine.com:993 POP3 mail.elektrine.com:995 SMTP mail.elektrine.com:465
© 2026 Elektrine. All rights reserved. Server: 02:26:20 UTC