@boarders@mathstodon.xyz
@boarders@mathstodon.xyz avatar

boarders

@boarders@mathstodon.xyz

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

This profile is from a federated server and may be incomplete. Browse more on the original instance.

highergeometer, to random
@highergeometer@mathstodon.xyz avatar

@jared has a question about this paragraph, written by Frank Ramsey in 1925:

"The object of this paper is to give a satisfactory account of the Foundations of Mathematics in accordance with the general method of Frege, Whitehead and Russell. Following these authorities, I hold that mathematics is part of logic, and so belong to what may be called the logical school as opposed to the formalist and intuitionist schools. I have therefore taken Principia Mathematica as a basis for discussion and amendment ; and believe myself to have discovered how, by using the work of Mr Ludwig Wittgenstein, it can be rendered free from the serious objections which have caused its rejection by the majority of German authorities, who have deserted altogether its line of approach."
—Frank Ramsey, "The Foundations of Mathematics"

https://mathstodon.xyz/@jared/111032333299331107

I would have guessed that "German authorities" would surely include Hilbert, who was surely solidly in the formalist camp. And others developing set theory, for instance, instead of R+W's type theory. Weyl might be representative of the "German authorities" rejecting R+W in favour of intuitionism (he gets an early mention in the essay).

boarders,
@boarders@mathstodon.xyz avatar

@highergeometer do you know historically why Brouwer seems associated with Bolshevism? I looked into it several times, but I couldn’t seem to find anything regarding his political views or why his viewpoint was studied in parts of the Soviet Union

boarders, to random
@boarders@mathstodon.xyz avatar

"Technology is concrete and path-dependent and interacts with economic and social forces. The form it takes is essential to the effect it has"

https://www.youtube.com/watch?v=_0dc7qutyBc

acowley, to random

While I’m very much in favor of static analysis and types, I don’t enjoy seeing static vs dynamic debates flare up. When static type advocates speak of how helpful and empowering types are, there’s the usually unstated requirement that you be as adept at reasoning about types as they are. If someone is really dead set against learning how to work with them, a type checker may well not be super helpful.

boarders,
@boarders@mathstodon.xyz avatar

@acowley the debate - like many such debates - seems to attract people who can’t imagine any evidence/wisdom in favour of the opposing view (on both sides), and seem to see the issue as being straightforwardly connected to moral virtue. It is not only not about whatever scientific insights we might have about programming languages or programming, but not even about how we might rationally think about what programming is or could be and the differing functions we put it to

j2kun, to random
@j2kun@mathstodon.xyz avatar

I was going to write a short blog post giving my mental picture for why the definition of limsup/liminf is necessary and sensible, and pair it with some thoughts on how a well-timed, thoughtful picture in math can make your confusion disappear.

Then I found that the picture I had in mind was already on wikipedia: https://commons.wikimedia.org/wiki/File:Lim_sup_example_5.png

It's a sequence of points sampled from an oscillating sine wave with asymptotically decreasing amplitude, where the limiting amplitude is 1, but if you just used sup you'd get values bigger than 1, and the limit does not exist.

I remember spending a long time as a undergrad, before I even became a math major, coming up with this same picture on my own, and how many times it helped me in tutoring calculus/analysis students over the years.

boarders,
@boarders@mathstodon.xyz avatar

@j2kun this picture of the cantor set in terms of paths in an infinite binary tree: https://en.m.wikipedia.org/wiki/File:Cantor_set_binary_tree.svg

boarders, to random
@boarders@mathstodon.xyz avatar

"The algorithm-proof world would resemble a vast swathe of frozen porridge, or perhaps large stretches of Nebraska, in which every place is much like any other and nothing ever happens."

https://aeon.co/essays/discretion-is-hard-to-live-with-even-harder-to-live-without

boarders, to random
@boarders@mathstodon.xyz avatar

General question: does it still
make sense to speak of “metamathematics” as distinct from parts of categorical algebra, topos theory, type theory etc? In the early 20th century is seems to refer exclusively to meta-theoretic parts of axiomatic systems used to formalize mathematics, however we seem to have a much more algebraic / pluralistic view now about what “foundations” means

boarders,
@boarders@mathstodon.xyz avatar

@mw I’m afraid I haven’t a clue what this means

sc_griffith, to random
@sc_griffith@mathstodon.xyz avatar

no

boarders,
@boarders@mathstodon.xyz avatar

@sc_griffith this is why I love mathematics

oantolin, to random
@oantolin@mathstodon.xyz avatar

I can't believe I never noticed before that the fundamental group of a join of non-empty spaces is always free. If X and Y have m and n components respectively, then the fundamental group of XY is free on (m-1)(n-1) generators. I think I only knew the case where m or n is 1, where XY is simply connected.

boarders,
@boarders@mathstodon.xyz avatar

@oantolin this is a nice fact (and one I also didn’t know), but I haven’t quite yet convinced myself why it is true (I think one can probably directly give the cells of a CW complex of the join, but somehow I don’t think this is a nice way to think of it)

boarders,
@boarders@mathstodon.xyz avatar

@oantolin a very slick argument :)

boarders,
@boarders@mathstodon.xyz avatar

@oantolin this was actually the only part that I figured out - that if both are non-empty then the cone on X or Y sits inside the subspace and so you can contract any path lying in X or Y

deech, to random
@deech@mastodon.social avatar

Esolang where literally everything is called functor

boarders,
@boarders@mathstodon.xyz avatar

@deech the functor module signature is a functor for endomap on which we might make it into a functor by writing fmap by overloading the operator()

alexr, to random

So how free could a monad be, in principle? Could you make them even freer, if you wanted? Or are these as free as we're getting?

boarders,
@boarders@mathstodon.xyz avatar

@chrisamaphone @alexr “obedience to a law one has prescribed for oneself is freedom” - Rousseau thinks the answer is algebras

boarders, to random
@boarders@mathstodon.xyz avatar

“Philosophers today are as fond as ever of apriori arguments with ethical conclusions. One reason such arguments are always unsatisfying is that they always prove too much; when a philosopher 'solves’ an ethical problem for one, one feels as if one had asked for a subway token and been given a passenger ticket valid for the first interplanetary passenger-carrying space ship instead.”

chrisamaphone, to random
@chrisamaphone@hci.social avatar

me clicking “show more” on a post from a server with no length limit: i have been tricked into reading a blog post. how dare

boarders,
@boarders@mathstodon.xyz avatar

@beka_valentine @chrisamaphone incredibly punishing memories from 2013 of reading that utter drivel

typeswitch, to random
@typeswitch@gamedev.lgbt avatar

thinking about separating representation types from reasoning types

boarders,
@boarders@mathstodon.xyz avatar

@typeswitch @MartinEscardo lean4 has some of this idea (i.e. using C arrays to represent lists in compiled programs). The thing I would like with this is some kind of process of formal refinement where I can construct a program by some specification of pattern matching and I can allow certain type refinements of an interface that meet this specification. I think this is a kind of (somewhat unfulfilled )vision of algebraic programming offered by ML-style modules.

boarders, to random
@boarders@mathstodon.xyz avatar

A strange dogma that entered parts of culture through analytic philosophy is the notion that some special status is afforded a view which is presented in the form of a collection of premises and conclusion (all in quasi-legalistic ordinary language) in some ambient logic which is not to be further commented upon.

This is transformed from the reasonable seeming view that clarifying constituent parts of an argument can help us to understand the stakes of a debate/position and to clarify which aspects of a worldview are in play, into the view that doing this performance demonstrates some higher adherence to truth or some higher standards of rigour. I see no reason why stories, myths, parables, dialogues, aphorisms, argumentative essays etc. cannot be as good or better at investigating some question than pretend logical syllogisms.

boarders,
@boarders@mathstodon.xyz avatar

“The extreme deductivism of much contemporary analytic philosophy may reflect the grip of the problem/solution metaphor”

chrisamaphone, to random
@chrisamaphone@hci.social avatar

do you have an onion opinion

boarders,
@boarders@mathstodon.xyz avatar

@chrisamaphone hard to articulate as it is very multi-layered

jntrnr, to random

Something I'm noticing in comments to my recent blog post on #nushell is that a lot of folks have a strict separation between interactive shell and scripting.

When I point out in the post that Nushell is really meant to scale smoothly between the two, some folks say things like "so you're saying it's really a scripting language not a shell"

I want to help folks see they don't have to choose. They can scale ideas all the way up in one language without rewriting.

boarders,
@boarders@mathstodon.xyz avatar

@jntrnr if it is a scripting language, then I would say it resolves the fundamental tension of scripting langauages, which is to treat pipes and processes as a kind of ffi interface which we can marshall data and invocations back and forth to but which are fundamentally separate. Scripting langauages (other than something like #lang rash, in racket) don’t seem to have resolved this distance between other process calls, environment variables etc. and those things which lie firmly within the programming language.

I think one reason people are resistant to these kinds of programming environments is that current thinking on language design has led to a kind of dogma of responsibilities- you should read data from the “outside world” - keep it inside the sealed off world of the programming language for as long as possible, and then convert back to something the outside world speaks. It is not as though this isn’t in some sense a good model or “true”, but there is no reason not to question it as a fundamental design principle (as excel, smalltalk, common lisp and nushell all, to some extent, do in my mind)

wilfredh, to random
@wilfredh@mastodon.social avatar

Rust is the only language I can think of with a first party version switcher. rustup is maintained by the core team, unlike rvm or nvm.

Are there other languages like Rust in this respect?

boarders,
@boarders@mathstodon.xyz avatar

@wilfredh perhaps ocaml with opam

todd, to random
@todd@mathstodon.xyz avatar

Hello everyone! I have arrived on Mathstodon now.

If you're in the fortunate position of not knowing me, I am a Teaching Fellow and (until my corrections are done) Ph.D. student at the University of Birmingham, in the School of Computer Science's Theory Group. I am interested in constructive mathematics, univalent type theory and Agda.

My first bit of news is that yesterday I successfully defend my thesis (subject to minor corrections), which concerns formally reasoning in Agda about search algorithms on types for exact real numbers. I was supervised by Dan Ghica and @MartinEscardo.

boarders,
@boarders@mathstodon.xyz avatar

@todd really looking forward to reading it after your excellent related blog posts! Congrats and good luck for what lies next!

jonmsterling, to random
@jonmsterling@mathstodon.xyz avatar

Today is my first day of work as Faculty! Wish me luck

boarders,
@boarders@mathstodon.xyz avatar

@jonmsterling good luck Jon! Make your own history :)

zanzi, to random
@zanzi@mathstodon.xyz avatar

I was pretty excited that HoTT has finally started to click for me, but the neverending joyless comments that I need to rename my monoids to pointed magmas is killing any interest in the topic

boarders,
@boarders@mathstodon.xyz avatar

@zanzi I understand the frustration. What helps me is to understand that social media as a technology creates some sense of immediacy without any of the usual context that accompanied immediacy. People will assume an idle observation or scratchpad thought is some kind of official record of note or tally of your knowledge.

boarders, to random
@boarders@mathstodon.xyz avatar

In the same way as we should (or have) do(ne) away with the dualisms of analytic vs synthetic, fact vs value and empirical vs theoretic (and doing away with a dualism doesn’t mean doing away with all relevant distinctions), I think it is worth questioning the dualism of formal vs informal. We reason about “formal” systems by meta-theoretic principles which are arrived at via informal reasoning or informal arguments. It is not clear what the meaning of “can be formally proved in principle” is in almost all cases, and it is not clear that it is valuable in itself. There remains value in the idea of more reliable or truthworthy knowledge and in the immense capacity formal systems seem to grant us.

  • All
  • Subscribed
  • Moderated
  • Favorites
  • •
  • JUstTest
  • rosin
  • mdbf
  • osvaldo12
  • ethstaker
  • tacticalgear
  • DreamBathrooms
  • thenastyranch
  • magazineikmin
  • modclub
  • Youngstown
  • everett
  • slotface
  • kavyap
  • megavids
  • GTA5RPClips
  • khanakhh
  • cisconetworking
  • tester
  • ngwrru68w68
  • normalnudes
  • Durango
  • InstantRegret
  • cubers
  • provamag3
  • anitta
  • Leos
  • lostlight
  • All magazines
    •