espeed

Here's an eclectic mix of examples from various perspectives across multiple domains. Understanding the representation of knowledge and the fundamental structure that underpins the connective essence of things is one of the prime ideas that drives my thinking, and as a consequence much of what I post about on here is related to that in some way. Below is a brief sampling of examples related to this idea, and for a more extensive list, browse through my postings (and if you can see how they all connect, let me know!).

In general, see the Classification of Finite Simple Groups [0]. In terms of specific examples, the minimal classifications of knots [1], trees [2], and braids [3] are 3 instances that popped to mind. From a number-theoretic perspective, the paper Enumerating the Rationals and its derivative works are interesting reads. In terms of spatial structure and spatial decomposition, look at the classification of crystal structures [4], lattices, polytopes (zonotopes are particularly interesting), periodic and aperiodic tilings, the classification of space-filling curves, and the classification of closed surfaces [5]. From a relational perspective, look at the classification of topological spatial relations [6] and Allen's interval algebra [7]. And the one my intuition finds most intriguing is the classification of Group Theory Single Axioms and its relation to my conjecture that division is primary.

[0] Classification of Finite Simple Groups https://en.wikipedia.org/wiki/Classification_of_finite_simpl...

[1] Prime Knots https://en.wikipedia.org/wiki/List_of_prime_knots

[2] Enumerating Trees https://www.cs.virginia.edu/~lat7h/blog/posts/434.html

[3] Braid Group https://en.wikipedia.org/wiki/Braid_group

[4] Crystal Structure https://en.wikipedia.org/wiki/Crystal_structure

[5] Classification of Closed Surfaces https://en.wikipedia.org/wiki/Surface_(topology)#Classificat...

[6] Topological Spatial Relations https://en.wikipedia.org/wiki/Spatial_relation

[7] Allen's Interval Algebra https://en.wikipedia.org/wiki/Allen%27s_interval_algebra

[8] "Yet Another Paper on Group Theory Single Axioms" https://www.cs.unm.edu/~mccune/projects/gtsax/

P.S. Clifford Algebra / Geometric Algebra [00] unifies much of mathematics, e.g. in GA, Maxwell's equations can be reduced to one equation and expressed on one line [01]:

[00] Geometric Algebra https://en.wikipedia.org/wiki/Geometric_algebra

[01] Maxwell's equations formulated in terms of Geometric Algebra https://en.wikipedia.org/wiki/Mathematical_descriptions_of_t...

I linked to some of the key research findings in this comment: https://news.ycombinator.com/item?id=18307333

Are you referring to clumps of hair falling out on a woman, or male-pattern baldness?

MBA curriculum is geared for people who will be managing medium to large established companies, not so much about the stuff you need to know when founding a company. Founding teams of 2 or 3 should possess foresight that led to a visceral understanding of the problem, the insight that led to the discovery of the secret to solving it -- that rare and valuable perspective that lights the path that no one else sees -- the verbal fluency to communicate what they see, and the technical expertise to implement it. Rarely is this skillset possessed all by one person, and the workload will be great, so that's why teams of 2 or 3 are recommended.

Founder skill sets should complement each other, but that doesn't mean one needs to be an MBA. Unless it's a case where it's founder who has pondering the problem for years, is the source of the insight ,and they just happen to have an MBA too, investors tend to view MBA founders as a net negative [0] vs strong technical team.

Ideally you want a brilliant generalist who sees the big picture to communicate and lead, someone who can speak both languages (tech and business),Often it's someone with a strong tech background who has grown up in an entrepreneurial family or lived in an entrepreneurial environment long enough to absorb the language and a tacit understanding. Paired with a co-founder who has deep, specialized, world-class expertise and a world-class engineer who loves to code, that's a strong team.

Don't worry about scaling to 10,000 employees before you've even begun. That will be a great problem to have when the time comes, and by then you'll the funds to hire a team of MBAs. You outsource your legal and accounting to specialized firms. When you're ready to raise funds, find a good startup attorney to set up the corp, and they'll who the good accountants are -- ask them to recommend. Until then, focus on your team and the core problem you're trying to solve, understand it from every angle -- from the perspective of multiple domains -- until you see the way it all aligns.

Beyond that, read Paul Graham's essays, absorb the Startup School lectures, and read Zero to One:

* http://www.paulgraham.com/articles.html

* https://www.startupschool.org/

* http://zerotoonebook.com

[0] http://startupclass.samaltman.com/courses/lec03/

Someone introduced me to Conal's work a few days ago and recommended I watch his "Compiling to Categories" talk which I hadn't seen, and it just so happened that I watched it earlier today before this talk/paper posted. After viewing both for the first time today and reviewing the corresponding papers, one thing jumps out that's certain, and you can see it crystal clear. Conal is brilliant. And I don't say that lightly. The clarity of his work and his perspective on the problems is pristine. It's rare when someone is able to cut through the noise and peer into to the essence because there's no map and it's so hard to achieve the level of clarity that allows you to see the path that breaks through, but somehow he found the insight and nailed it. Damn, well done!

I did too a few years back, and it clouds the brain no-doubt. It got to the point where something had to be done, and so I set everything aside and dedicated 6 months to figuring out how to fix it.

Read this book: Spark: The Revolutionary New Science of Exercise and the Brain by John Ratey (http://en.wikipedia.org/wiki/John_Ratey), the professor of psychiatry at Harvard Medical School.

I have posted on the effects of sprints several times over the years so rather than repost again, here's a link to the threads: https://hn.algolia.com/?sort=byPopularity&prefix&page=0&date...

Running sprints were key, but inflammation due to diet was part of it too (a latent issue not widely discussed, but a factor more common than you might think). I solved that by eliminating certain foods one by one that are known to cause inflammation. Peanuts were one, and eliminating aspartame (diet coke) had a noticeable effect within just a few days (I verified it wasn't the caffeine by adding back tea and coffee, and those had no noticeable effect).

Here's some links to the original Harvard and USG research findings on the issues with aspartame and artificial sweeteners/flavors in general, like why it's banned it baby food: https://news.ycombinator.com/item?id=6703802

Here is a link to the corresponding SIGMA 2018 paper and a link to the video shown at the end of the talk, which shows an animation illustrating the conjectures in the paper.

An animation illustrating the conjectures [video] https://www.youtube.com/watch?v=Ru0Zys1Vvq4

The Intro begins...

  These conjectures resulted from our attempts to
  understand data obtained following a 9 month
  calculation in magma on a supercomputer at the MPIM
  in Bonn. These results go far beyond existing 
  calculations and are obtained using a new algorithm.
  The algorithm relies in an essential way on ideas of 
  Libedinsky, Riche and the second author. The behaviour 
  we observe appears highly non-trivial, which suggests 
  that proving anything might be difficult.

Billiards and Tilting Characters for SL3 [pdf]

http://emis.ams.org/journals/SIGMA/2018/015/sigma18-015.pdf

Here's the code: https://github.com/nykh/cs242-lambda-pi

Carl Jung termed the phenomenon synchronicity [1], "which holds that events are 'meaningful coincidences' if they occur with no causal relationship yet seem to be meaningfully related." Google the philosophy of information, phenomenology, and "the world is made of meaning." Also related is the phenomenon of multiple discovery / simultaneous invention [2]. Ironically, this is in-part what the Curry–Howard correspondence is about, with the Church–Turing thesis being a prime example [3].

[1] https://en.wikipedia.org/wiki/Synchronicity

[2] https://en.wikipedia.org/wiki/Multiple_discovery

[3] https://en.wikipedia.org/wiki/Church–Turing_thesis

My burgeoning conjecture (as hinted at in a previous comment) is that all can be unified, transformed, and optimized for modern hardware under the matrix model of computation -- type theory, the lambda calculus, the actor model, neural nets, graph computing -- I'm starting to see a path to where all models are aligned across vectors of unity.

Here are some the correspondences I've been looking at...

* Graph algos in the lang of linear algebra now realized and encoded into GraphBLAS [1]

* The three normed division algebras are unified under a complex Hilbert space [2]

* Ascent sequences and the bijections discovered between four classes of combinatorial objects [3]

* Dependent Types and Homotopy Type Theory [4]

* Bruhat–Tits buildings, symmetry, and spatial decomposition [5]

* Distributed lattices, topological encodings, and succinct representations [6]

* Zonotopes and Matroids and Minkowski Sums [7]

* Holographic associative memory and entanglement renormalization [8]

[1] Graph Algorithms in the Language of Linear Algebra (Jeremy Kepner) http://www.mit.edu/~kepner/ Discussion: https://news.ycombinator.com/item?id=18099520

[2] Division Algebras and Quantum Theory (John Baez) http://math.ucr.edu/home/baez/rch.pdf

[3] (2 + 2)-free posets, ascent sequences and pattern avoiding permutations [pdf] https://www.sciencedirect.com/science/article/pii/S009731650...

[4] Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities [pdf] https://www.cs.cmu.edu/~rwh/papers/cartesian/paper.pdf

[5] Bruhat–Tits buildings and p-adic Lie groups https://en.wikipedia.org/wiki/Building_(mathematics)

[6] Distributive lattices and Stone-space dualities https://en.wikipedia.org/wiki/Distributive_lattice#Represent...

[7] Solving Low-Dimensional Optimization Problems via Zonotope Vertex Enumeration [video] https://www.youtube.com/watch?v=NH_CpMYe3tw https://en.wikipedia.org/wiki/Zonohedron

[8] Entanglement Renormalization (G Vidal) https://authors.library.caltech.edu/9242/1/VIDprl07.pdf?hovn... Holography https://en.wikipedia.org/wiki/Holographic_associative_memory

Google Scholar: https://scholar.google.com/scholar?q=related:Yi-GtarGxh0J:sc...

Philip Wadler provides an in depth discussion on the Curry–Howard correspondence [0] in his paper Propositions as Types [1], and he has given several talks under the same name that are on YouTube.

The talk Prof Wadler gave at Strange Loop is the most cited, but the talk he gave at Stanford [2] is the most interesting because Carl Hewitt was in the audience and was challenging him on the merits and long-term viability of functional programming in general vs Hewitt's Actor Model [3] for scalable concurrent computing.

[0] Curry–Howard correspondence https://en.wikipedia.org/wiki/Curry–Howard_correspondence

[1] Propositions as Types [pdf] http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-...

[2] Propositions as Types (Stanford) [video] https://www.youtube.com/watch?v=ivzpaiw26wQ Slides [pdf] http://www.inf.ed.ac.uk/teaching/courses/tspl/pat.pdf

[3] Actor Model https://en.wikipedia.org/wiki/Category:Actor_model_(computer...

The significance of this paper is not about learning the λ-calculus.

Rather, to me the significance of this paper is that it presents a novel way of "implementing the lambda calculus in an algebraic system" and provides a correspondence between the λ-calculus and the matrix model of computation:

  Vector and matrix valued functions can be represented
  by vectors and matrices some of whose entries are 
  lambda expressions.

I have been looking for a lingua franca for programming languages, a way to unify the langs and make use of the decades of wisdom encoded into our langs' Great Libs. Maybe the matrix model and linear algebra is the lingua franca I seek.

NB: Better to refrain from saying stuff like "it completely misses the point" unless you are certain you understand the point beyond the level presented.

NB: the file command tries to identify file types via file sigs (magic numbers) stored in /usr/share/file/magic, for more mysterious file types or partials, you'll need to use one of the other methods.

NB: I suspect the number you are thinking of is a 2530 digit sequence on a 4-digit lock, not 153 on 5...

https://en.wikipedia.org/wiki/De_Bruijn_sequence#Uses

Yes, and in this case the sequence is specifically the "classic" De Bruijn sequence [1]; however, there are other sequences that bear De Bruin's name, such as the Moser de Bruijn sequence, which is the one I reference most due to its relation to Z-order curves and pairing functions.

[1] https://en.wikipedia.org/wiki/De_Bruijn_sequence

[2] https://en.wikipedia.org/wiki/Moser-de_Bruijn_sequence

Type-driven development, meta languages, specs, provably correct code, and automatic code generation were some of the big overlapping themes at Strange Loop [1] this year. All the talks posted online this week [2], and I've posted links to some of the related videos below [3].

It's a good indicator that the time has come for an idea when multiple lines of research and projects from disparate domains begin converging on the same idea from different directions.

Several facets of the puzzle I've been working the last few years have converged towards this area so it's good to see that it's not just me, maybe that means we're all on the right track. But as 'pron and those who have been working in this area have pointed out [4], this part of the puzzle is not yet solved, and one of the primary open issues is how to scale it to the system level (beyond provably correct programs to provably correct systems).

One of the questions I've been pondering is how can we combine provably correct software specs with hardware specs identified for any given system to find the optimal data structures and algorithms given the constraints of that architecture.

Does something similar already exist? What's the best software currently out there for simulating ideal data flow for a given hardware configuration and a given set of system constraints?

[1] Strange Loop https://www.thestrangeloop.com

[2] Strange Loop 2018 talks (80 videos) https://www.youtube.com/playlist?list=PLcGKfGEEONaBUdko326yL...

[3] Related videos...

* Vellvm - Verifying the LLVM, by Steve Zdancewic https://www.youtube.com/watch?v=q6gSC3OxB_8

* All the Languages Together, by Amal Ahmed https://www.youtube.com/watch?v=3yVc5t-g-VU

* Towards Language Support for Distributed Systems, by Heather Miller https://www.youtube.com/watch?v=IeBbiQZYmuY

* Data Driven UIs, Incrementally, by Yaron Minsky https://www.youtube.com/watch?v=R3xX37RGJKE

* Proof Theory Impressionism: Blurring the Curry-Howard Line, by Dan Pittman https://www.youtube.com/watch?v=jrVPB-Ad5Gc

* A Little Taste of Dependent Types, by David Christiansen https://www.youtube.com/watch?v=VxINoKFm-S4

* You are a Program Synthesizer, by James Koppel https://www.youtube.com/watch?v=ldkF-4WNZqA

[4] open issue is how to scale it to the system level https://news.ycombinator.com/item?id=18253680

> Good specifications are often written at a level that generating executable code from them is often undecidable and almost always intractable in practice.

What about modern dependently-typed meta languages like Idris and program synthesizers like Nadia Polikarpova's work on Synquid?

Type-Driven Program Synthesis, by Nadia Polikarpova (StrangeLoop 2018) [video] https://www.youtube.com/watch?v=HnOix9TFy1A

MIT Comcom: Synquid program synthesizer, and more command-line tools for the web

http://comcom.csail.mit.edu/comcom/

Idris Software Foundations https://github.com/idris-hackers/software-foundations

No hits??? Or no callbacks after first contact?

Send me your resume, and I'll take a look (email in profile).

Who are the founders?

What is their background?

What are they selling?

Who are they selling to?

No. That ship has sailed. The new runtime is in the browser. Learn about wasm and matrix-multiply-add.

No, don't think like that. Concurrency is becoming more important, that's just the new reality on the other side of Moore's Law. Concurrency doesn't just happen. Someone has to design the AWS Lambda concurrency model and build the system to scale even if it's not you. And unless the system's design is improving over time and approaching optimal, eventually no one's going to use it because it will cost more than it should so people will move on toward the optimal one. And just like we have multi-layer caching models, distributed means we now have multi-layer concurrency models. Message passing Actors might be optimal between nodes, but within nodes matrix-multiply tensor models running on GPU/TPU accelerators is where optimal's at. And unless you understand it, you won't even be on the map.

And that capabilities model is one of the big differences in Pony and was the key to achieving Pony's parallel lock-free provably correct concurrency model.

Most lang/system capability models (including Go's) are open from the start -- where anyone can do anything -- and then when designing the lang/system you try to restrict access between some things at some of the time, but this gets messy fast and it's hard to get right and thus it's almost never optimal.

So rather than trying to start with an open model that's inherently flawed by definition, Pony flips the model on its head and begins from the perspective that everything is denied unless specified. You would say Pony has a deny-first capabilities model, which you can see explicitly defined here in Pony's capabilities matrix...

https://soyyomakesgames.wordpress.com/2016/10/10/ponys-capab...

And if you listen to Sylvan's talks, he is emphatic that solving the capabilities problem upfront was key that made everything else possible. All the other cool stuff you hear about in Pony like the provably correct runtime and finally achieving something approaching Hewitt's elusive Actor model that's been theoretically true for 40 years but never fully realized. Well the key to solving that mystery and unlocking the door was to take a new view on the capabilities model and building everything off that from the start.

Pony's new novel lock-free Actor model is of considerable note. Sylvan (https://github.com/sylvanc) has since joined MSR Cambridge and is working on the distributed model now...

https://github.com/ponylang/ponyc

https://www.ponylang.io/discover/#what-is-pony

https://www.youtube.com/results?search_query=ponylang

You're referring to the distributed Actor model?

What lang ecosystem with an interactive REPL do you see as the best fit for pairing with and driving Pony?

I've been dreaming of ways to help bootstrap the Pony lang/lib interop story and build toward a numerical interactive programming environment, being able to combine Pony's native async Actor model and runtime safety guarantees, while also safely being able to hook into to an external ecosystems existing numerical computing, data structure, and GPU/TPU accelerator libs.

I seem to remember someone giving a lang talk a while back where in the Q&A the speaker said integrating with Pony might be a good fit. I was looking into dependent types at the time...it may have been Idris or OCaml, and hooking into the Julia ecosystem would be most interesting, with maybe even Zig acting like low-level LLVM glue code binding all the external C libs together.

In my dream I have it all and the Pony too! All the lang libs are hooked together in a typed-provable way, and when fully connected they combine to form a high-performance, interactive parallel distributed programming environment, and it runs in the browser too. What do you think, is that too much of a DeepDream?

One of the common traits is an inability to access higher-order cognitive functions such as empathy and being unaware of their inability to do so. This often means they're in a chronic state of anxiety and confusion because the intentions of others make no sense. Conflating empathy for low affect feelings of sympathy while assuming an identity of the most empathetic and most sympathetic person in the world, maybe even thinking they're HSP. Here's one way you can find out and discover to what extent that's factoring into the mix.

Next time you find yourself in a situation where they are behaving contrary to what you would expect, don't assume malice. Make sure you carefully and clearly articulate your feelings and perspective, have them voice their concerns, and then ask them to rearticulate what you just said. Ask them to put into their own words what you are thinking and feeling, to rearticulate what your perspective is and why. Ask them to explain the cause and effect of their actions. And then shut up and let them answer, see what happens. Pay close attention to how they respond, to what extent they can empathise even if it's just simply repeating back what you said. You both may be shocked -- them by the question, you by the response -- but it'll be an enlightening experience. And after a time or two of that, at least you'll know where you are.

Yeah, succinct data structures aren't something taught in most intro to data structures courses, and the concept may even be unfamiliar to oldhats since SDSs are relatively new on the scene -- the public datasphere only started becoming conscious of the idea in 1988 when Guy Jacobson introduced them in his CMU thesis. And I have yet to find a digital copy of it online so for those who want to read the original thesis, you may have to order a paper copy of one or go to the CMU library to read it.

https://scholar.google.com/scholar?q=guy+jacobson

But, there's been a lot of development on succinct data structures since, and this post on the fast select algorithm was in-part a continuation of a conversation from a post yesterday on succinct data structures in general and the open-source lib SDSL 2.0. So if anyone wants to learn more about SDSs in general, there's a bunch of links to videos and reference material in the comments of yesterday's thread...

SDSL – Succinct Data Structure Library 2.0 https://news.ycombinator.com/item?id=18204432

Yep, often misdiagnosed as BPD or one of the Cluster B's, come to find out Asperger's is on the same spectrum. One of the most confounding situations I've ever experienced.

https://en.wikipedia.org/wiki/Cluster_B_personality_disorder...

Well, if it's true, we finally have a real live answer to the age-old question in Iron Eagle: "Dad, will the Maverick fire if we're still on the ground?" [1]

https://en.wikipedia.org/wiki/Iron_Eagle

[1] https://www.imdb.com/title/tt0091278/quotes