Profile

Cover photo
Ashley Yakeley
99,022 views
AboutPosts

Stream

Ashley Yakeley

Shared publicly  - 
 
More suspicion of computationalism.

http://immanence.org/post/move-by-copy-and-delete/
"Ah, I see you've come to have your mind uploaded into cyberspace. Well come in. Think of a number and don't tell me what it is." "Um, OK." "Jolly good. Now lie down on that table with the scanning...
3
1
Frank Atanassow's profile photomathew's profile photoDan Piponi's profile photoFelipe Lessa (meteficha)'s profile photo
17 comments
 
> They wouldn't get to travel anywhere

That claim only makes sense for the tiny minority of people living on the backwater called Earth and who speak certain ancient dialects. For the rest of the galaxy there is no word that means "travel except via beaming" and most of the Galaxy would find such a word about as useful as a word that meant "two, except when counting apples".
Add a comment...

Ashley Yakeley

Shared publicly  - 
 
One of the problems of not being trained in mathematics is that even when I have a rigorous proof in my head, I have trouble writing it down in a way that mathematicians can read without scratching their heads.

I've been learning Coq, but that may be possibly worse in this regard.
3
Dan Piponi's profile photoAshley Yakeley's profile photoBenjamin Russell's profile photoMarco Devillers's profile photo
4 comments
 
Having worked with another proof tool, PVS, I simply gave up. The tool insisted on introducing type constraints at the strangest corners of proofs, so I ended up just being led by the tool.

Probably was a lousy formalization I was working in anyway. Should have terminated my work on it earlier.
Add a comment...

Ashley Yakeley

Shared publicly  - 
 
Having a big argument with Coq. These arguments tend to end the same way, with me suddenly realising where I'm wrong. It's like arguing with God in the Jewish tradition.

(In this case, I told Coq that a Lattice is a PartialOrder with some stuff, and a BoundedPartialOrder is also a PartialOrder with some stuff, and a BoundedLattice is a Lattice and a BoundedPartialOrder, but Coq won't let me do anything useful with BoundedLattice because I haven't shown it that the two implied PartialOrder instances are the same.)
#Coq #DiamondOfDeath  
3
1
Alexey Romanov's profile photo
Add a comment...

Ashley Yakeley

Shared publicly  - 
 
I have a special fondness for the Monoid and Applicative classes. Sometimes if you're wrestling with a type, trying to write it to best capture the semantics, if you can somehow make it an Applicative, with all the laws correct, everything else will magically fall into place.

The same thing often applies to Monoid (for kind * of course), though to a somewhat lesser degree.
3
Add a comment...

Ashley Yakeley

Shared publicly  - 
 
I just realised that git repositories would be an excellent example of Goguen-style causality topologies. A set of commits S is open iff for every x member of S, all ancestors of x are members of S. Not sure if this means anything useful though.

https://plus.google.com/u/0/+AshleyYakeley/posts/fKnXWr1DiE5
1
2
Shachaf Ben-Kiki's profile photoAshley Yakeley's profile photoAlexey Romanov's profile photoKisho Shin (illumi23)'s profile photo
2 comments
 
Yes, thank you. I'm self-taught in mathematics so there are big holes in my knowledge.
Add a comment...

Ashley Yakeley

Shared publicly  - 
 
Some gorgeous typography for maths lecture notes. Though I think it would better with block paragraphs rather than indents.

Nine Chapters on the Semigroup Art
http://www-groups.mcs.st-andrews.ac.uk/~alanc/teaching/m431/c_semigroups_a4.pdf
6
Dan Piponi's profile photorif a. saurous's profile photo
2 comments
 
There are a few tips on the last page.
Add a comment...

Communities

5 communities

Ashley Yakeley

Shared publicly  - 
 
An argument against computationalism.

http://immanence.org/post/are-we-being-simulated-by-a-clock/
Are we living in a simulation? I don't mean the brain-in-a-jar (or body-in-a-pod) kind of simulation shown in The Matrix. I mean, is our whole universe, including our brains and minds, being simula...
1
Dan Piponi's profile photoJoshua Ball's profile photoAshley Yakeley's profile photomathew's profile photo
4 comments
mathew
 
This kinda reminds me of the fact that pretty much any file can be losslessly compressed to 1 bit, as long as you allow for a suitably special purpose decompression program.
Add a comment...

Ashley Yakeley

Shared publicly  - 
3
1
Ashley Yakeley's profile photoJim Stuttard's profile photo
 
I've been trying to formalise mathematics in Coq as a way of learning it rigorously, but it's been tough going.

https://github.com/AshleyYakeley/maths
Add a comment...

Ashley Yakeley

Shared publicly  - 
 
To understand what something in source code does, try deleting it and see what breaks.
5
Erik de Castro Lopo's profile photoDan Piponi's profile photoAshley Yakeley's profile photo
4 comments
 
They're objections the compiler raises to our arguments.
Add a comment...

Ashley Yakeley

Shared publicly  - 
 
Obviously I want to track the upstream branch with the same name. Always. Come on, git.
2
mathew murphy's profile photoSean Leather's profile photoMichael Weber's profile photo
3 comments
 
git checkout foo does that for me, though.
Add a comment...

Ashley Yakeley

Shared publicly  - 
 
Have I mentioned how much I hate Gerrit? One-review-per-commit is the wrong abstraction, with these leaks: not only does it force squashing when you, you know, have multiple commits you want to review, you have to go through all this "change-id" folderol when you want to update the review in response to comments.

A code review consists of a number of changes, each built on the last. Git already has this concept, it's called a branch. A sensible code-review system would simply let you specify which branch you wanted to merge into which other branch, and review based on the (fast-forward) difference. Want to update your review? Just push to the branch.
* Multiple commits per review
* No special references to push to
* Easy updating
Simple.

http://bitquabit.com/post/code-reviews-and-bad-habits/
1
Michael Weber's profile photo
 
Occasionally, you find people talking about the "Gerrit Topic" feature, which should allow just that, http://gitenterprise.me/2014/07/07/gitminutes-30-luca-milanesio-on-gerrit-code-review/

Hasn't happened yet, though.
Add a comment...

Ashley Yakeley

Shared publicly  - 
 
I am a beautiful person making a beautiful web site. And I'll be sure to drink plenty of water and not lean over too much until I've fixed that bug.
3
Erik de Castro Lopo's profile photoSean Leather's profile photoAlex Fink's profile photo
3 comments
 
You wrote this post by repeatedly selecting the first word suggestion on Swiftkey AICMFP.
Add a comment...
Communities
5 communities
Links
Contributor to
Story
Tagline
Bloody Brilliant.
Apps with Google+ Sign-in
  • Monument Valley