Remote

Boarders

@boarders@mathstodon.xyz

mastodon 4.7.2

Interested in mathematics (homotopy theory, category theory, topos theory), programming languages, and philosophy.

598 Followers

986 Following

25 Posts

Joined November 10, 2022

Site:

https://boarders.github.io

Locations:

NYC

Path:

What hope is there in a book about a book

Boarders @boarders@mathstodon.xyz

· 5mo ago

Replying to

@julesh The thing I do agree with is there is an emerging discipline of "information science" which one could imagine includes some array of: statistical learning, information theory, theoretical neuroscience, markov processes + martingales, complex systems theory, signal processing, machine learning, nascent science of machine learning + NN interpretability, machine vision etc. I don't agree with the idea that typical computer science is dead or the traditional subjects taught are no longer valuable, nor that it is ahistorical to keep going with this discipline. The main changes I would like to see is a greater emphasis on formal scientific knowledge, formal methods, verification etc. and less on thinking teaching should primarily have the instrumental purpose of operating as trade school for massive corporations that don't even provide funding for the pleasure of dictating the curriculum

12

3

1

0

Boarders @boarders@mathstodon.xyz

· 6mo ago

wrote a blog post, mostly to try to get back in the habit of public writing and to resurrect my blog. It uses agda-categories to give show semantics for STLC in a CCC. The very end has a few things that I will return to finish, but wanted to his publish in any case: https://boarders.github.io/posts/stlc-semantics.html

[apologies for the bad taste and quite hacky agda syntax highlighting, it is on my TODO list to do something better]

boarders.github.io

Semantics of STLC in Agda

Callan McGillx

15

0

6

0

Boarders @boarders@mathstodon.xyz

· 6mo ago

finished up an old post I had on well-founded relations and induction principles in agda: https://boarders.github.io/posts/well_founded_induction.html

boarders.github.io

12

1

3

0

Boarders @boarders@mathstodon.xyz

· 5mo ago

Replying to

@pigworker "just because you can play the [rocq] videogame doesn't mean you know type theory" - bob harper

8

3

0

0

Boarders @boarders@mathstodon.xyz

· 5mo ago

I generally subscribe to a loose version of Penelope Maddy’s notion of mathematical naturalism on philosophical questions in mathematics. If someone wants to debate whether 0 is a natural number or flavours of finitism, but they don’t have any connection with mathematical practices (new or old), then it has no cash value, and I have no interest in discussing it

5

2

1

0

Boarders @boarders@mathstodon.xyz

· 5mo ago

Replying to

@julesh what would you see as the curriculum containing what you think of as core knowledge, and which couldn’t be captured by an upper level course in an existing cs/maths degree?

5

10

0

0

Boarders @boarders@mathstodon.xyz

· 4mo ago

Replying to

@rntz@recurse.social I don’t really know if it is the kind of thing you have in mind but there is a nice discussion of por in Mitchell’s foundations of programming languages

3

1

0

0

Boarders @boarders@mathstodon.xyz

· 5mo ago

Replying to

@byorgey@mathstodon.xyz i do still think you’re a wizard, but fortunately my sanity is slightly restored that it doesn’t take 750 lines of agda to prove the fundamental theorem of algebra

4

3

0

0

Boarders @boarders@mathstodon.xyz

· 6mo ago

Replying to

@hallasurvivor very fun observation! I also can't quite figure out what goes wrong precisely. I think you can do some version of euclidean division on the quaternion polynomial ring, but that doesn't seem to imply it is a UFD

4

3

0

0

Boarders @boarders@mathstodon.xyz

· 5mo ago

Replying to

@zanzi@mathstodon.xyz my impression is mainstream media has thoroughly covered that traditional CS is useless and dead knowledge - I hear little else online

3

6

0

0

Boarders @boarders@mathstodon.xyz

· 5mo ago

Replying to

@cbaberle @pigworker that’s totally reasonable

3

0

0

0

Boarders @boarders@mathstodon.xyz

· 5mo ago

Replying to

@jonmsterling KB had a very good example of this in a recent talk where he asked an LLM to formalize something about Hilbert modular forms and in the _definition_ it asked for the underlying function not to be holomorphic (the actual def) but continuous

3

0

1

0

Boarders @boarders@mathstodon.xyz

· 6mo ago

Replying to

@codyroux @hallasurvivor unless I am mistaken I think can always inductively remove the leading coefficient of what I am trying to divide

3

1

0

0

Boarders @boarders@mathstodon.xyz

· 5mo ago

Replying to

2

0

0

0

Boarders @boarders@mathstodon.xyz

· 5mo ago

Replying to

@mnl@hachyderm.io lots of mathematics classes I imagine you could now also easily run experiments or get ways to visualize various phenomena which makes me think the core discipline and real scientific lessons are more valuable

2

1

0

0

Boarders @boarders@mathstodon.xyz

· 5mo ago

Replying to

@zanzi@mathstodon.xyz enrollments are hugely down due to all of the scare stories about how “CS is dead”

2

1

0

0

Boarders @boarders@mathstodon.xyz

· 5mo ago

Wrote a post on Kripke and Beth semantics in lean 4, and added some features to my blog so that you can see the proof state on hover: https://boarders.github.io/posts/beth.html

boarders.github.io

2

1

1

0

Boarders @boarders@mathstodon.xyz

· 5mo ago

Replying to

@ToucanIan I am just saying that a polynomial functor is a sum of representables, but neither the sum nor the representables need to be finite so X^Nat or 1 + X + X^2 + … are both “polynomial”

1

0

0

0

Boarders @boarders@mathstodon.xyz

· 6mo ago

Replying to

@andrejbauer what if is Lambek pointing out that Platonism, Formalism and Intuitionism can finally all be reconciled in the free topos?

1

1

0

0

Boarders @boarders@mathstodon.xyz

· 19mo ago

IEEE Has a Pseudoscience Problem:

http://deevybee.blogspot.com/2025/02/ieee-has-pseudoscience-problem.html

deevybee.blogspot.com

BishopBlog: IEEE Has a Pseudoscience Problem

6

0

10

0

Boarders @boarders@mathstodon.xyz

· 8mo ago

If anyone is interested in joining a cat theory reading group in NYC: https://bsky.app/profile/kirancodes.me/post/3mcsk7skqfs2n

1

0

0

0

Boarders @boarders@mathstodon.xyz

· 8mo ago

@krismicinski@types.pl the end point of the academy as exclusively free (read: very expensive) job training is that eventually the important decisions are all made by bean counters

0

0

0

0

Boarders @boarders@mathstodon.xyz

· 5mo ago

Replying to

@ToucanIan @pigworker polynomial is a pretty terrible name though, since you inevitably have to explain that you also allow the analogue of formal power series

0

4

0

0

Boarders @boarders@mathstodon.xyz

· 5mo ago

Replying to

@ToucanIan is the exponential function a polynomial?

0

2

0

0

Boarders @boarders@mathstodon.xyz

· 5mo ago

Replying to

@byorgey@mathstodon.xyz did you use an already existing implementation of the real numbers or use a way to state it that doesn’t need that?

0

1

0

0