Andrej Bauer - Models of intuitionism and computability

I got a bit lost there, ... but it does sound like there are a lot of things you can say about computability beyond just that "uncomputable functions exist".  It also sounds like Andy Pitts doesn't like modal logic.  I wonder what the quote was that he ended the talk with. I think it was something Jaap Van Oosten wrote somewhere. See Basic subtoposes of the effective topos (2013) by Sori Lee and Jaap van Oosten.

Subscribe to De KNAW.

Here's a May 2022 talk on the countable reals.


Subscribe to Topos Institute.

After listening to these two talks last night I dreamed that someone was explaining to me how you could build computational circuits using a kind of "coclocking". In this scheme the clock was an index into a type which was the successive ticks, and it meant that there was a notion of continuity in temporal evolution which was not the sort of thing Albert Einstein would have immediately understood. It was a really interesting dream! See David Albert Talking Complete Nonsense. Then I had another dream where I was part of a church community somewhere that reminded me of the Unitarian church I attended in Shreveport, Louisiana, except there was a bit more going on. It was really good. We were messing around with some contraption on a sports field, I think. 

Comments

Post a Comment

Popular posts from this blog

Steven Johnson - So You Think You Know How to Take Derivatives?

Image
A derivative is linearisation, and differential calculus is essentially linear algebra, ...  See  Freya Holmér - Why Can't You Multiply Vectors?  and  Freya Holmér on Continuity of Splines . See also the MIT OCW page:  Matrix Calculus For Machine Learning And Beyond  (Alan Edelman, Steven G. Johnson) Subscribe to The Julia Programming Language . Alan Edelman talking about expressing mathematics as computer code. The idea is that you can use computer languages to communicate mathematical ideas precisely to other people. See my comments about functional programming languages here:  https://prooftoys.org/ian-grant/hm/ Subscribe to TEDx Talks .
Read more

Tensor Fields and Simplicial Complexes

Image
Listening to Freya Holmér last night I started to get glimmers of an idea I had long ago about how to represent vector spaces in computational processes using this recursive abstract type :  abstype 'a point = POINT   of {getx :  'a vector,       diff :  'a point -> 'a point,       move :  'a point -> 'a point,       scale : 'a -> 'a point,       proj :  'a point -> 'a} with    fun new i (op +) (op -) (op * ) dot =    let fun self x =  POINT       {getx = x,        move = fn (POINT pr) =>           (self (x + (#getx pr))),        diff = fn (POINT pr) =>          self (x - (#getx pr)),        scale = fn i =>          (self (x * i)),        proj = fn (POINT pr) =>     ...
Read more

FUTO FUBS

Image
I think this is the first time they've actually publicly announced anything about this project. See these posts: Eron Woolf on Why Open Source is Failing Matt Mikhailov and Vincent McKibbon on The Problem with Open Hardware Jason Kridner talking About BeagleBoard.org and Software Development .  See these places:  https://danielc.dev/rk/ https://github.com/petabyt/rk https://github.com/futo-org/ret See also  https://pine64.org/devices/pinebook_pro/ . Subscribe to  FUTO .  See  https://github.com/nir9/low-level-learning-resources/tree/master/setups/debian . Subscribe to  Nir Lichtman .  If you're looking for a cool init process, try  https://ctx.graphics/terminal/ . See  Artful Bytes - When to Use a RTOS  and  How to Create a Successful Open Source Project . 
Read more