> There's also a huge issue with your use of the word subjective - math is objective. Proofs remain stable whether it's humans or any other system that does the processing. We test that objectivity by comparing the subjective readings from individual humans, and if the tests all return the same results, we can confidently say that the resulting proof is an objective fact about reality. Subjective fundamentally means that depending on the subject, the reading might change. Modern systems of math are formally, provably objective.
You are of course free to believe in mathematical Platonism, but that doesn't mean that non-Platonists would agree that proofs amount to objective "facts" about reality. And you are equally free to "prove it for yourself", which will just end up begging the question unless you are a Platonist.
That's not to say that math is subjective. But claiming that math is producing objective facts ignores at least a few hundred years of philosophy of mathematics (if not more). Even practicing mathematicians like Chaitin have described math as being more about inventing than discovering.
Holding a non-Platonist position also doesn't immediately lead to the sort of constructivist / "anything goes" position that some people ascribe to it, where you'd suddenly lose the ability to say that 2 + 2 = 4 and not 5. There are lots of philosophical positions that would agree that 2 + 2 is 4 without also claiming that this makes it a "fact" about any sort of objective reality or Platonic discovery.
Badlands and Days of Heaven are definitely his most conventional films and thus good starting points. Badlands especially is a great film, Days of Heaven is a bit uneven in terms of plot and pacing, but the cinematography is beautiful.
Then you have The Thin Red Line and The New World, which to me feel like a transitional period between the more conventional films and The Tree of Life, which is the first film that is characterized through and through by Malick's extremely divisive style. I personally love The Thin Red Line, but I can see why it's not for everyone. (I would skip The New World.) All later films have a very recognizable style, for which I think The Tree of Life is the best starting point.
Long story short: I'd start with Badlands, then watch The Thin Red Line, then The Tree of Life. If you like the last one, watch any of his later films.
Hey Sergio! I applied for the role of founding engineer a couple of months ago and passed the different stages. We had even been talking about the exact salary package and start date, decided to talk again in a couple of weeks about the specifics, but then I never heard back, despite reaching out to you again.
It’s totally fine if plans change and you decide not to move forward with a candidate, but I think a short email isn’t too much to ask after spending multiple hours on the various interviews.
That said, the interview process was otherwise pretty good and the work you’re doing sounds really interesting, so I would still encourage others to apply. Best of luck with Formal!
The linked pdfs on that page are wonderful. I reread Wirth's Plea for Lean Software and it still holds up remarkably well. It reminded me of Alan Kay's VPRI and the STEPS Toward the Reinvention of Programming which unfortunately ended in 2012. Oberon also doesn't seem to be actively developed anymore as far as I can tell. Are there any similar projects that are still being actively worked on?
Are there any "guided" walkthroughs for someone who has never used Oberon (or any of its later versions like Bluebottle or A2) that demonstrate its most unique UI/UX aspects? Something along the lines of Russ Cox' Tour of the Acme Editor[0] but for Oberon?
Oberon seems fascinating and I would like to eventually play around with it in an emulator, but any resources that show how it's being used (as opposed to a description of its design like in Wirth's book for example) would be appreciated.
Not all of those abstractions are equally leaky though. Automatic memory management for example is leaky only for a very narrow set of problems, in many situations the abstraction works extremely well. It remains to be seen whether AI can be made to leak so rarely (which does not meant that it's not useful even in its current leaky state).
Since all programs have to be compiled to boolean gates and these gates have to be encrypted, there is a difference of a few orders of magnitude between running programs natively on a CPU (which can of course use highly optimized arithmetical instructions) and running programs over MPC.
In the end, it all depends on the complexity of the program: For simple programs like the Wordle guess/solution comparison (about 40 lines of code, compiled to < 2k gates) the communication overhead is more significant than the computational overhead. The Garbled Circuits protocol used by Tandem needs 7 rounds of communication, so with a round-trip time of 50ms the whole execution takes 350ms.
For more complicated programs, the computational overhead becomes a bit more significant. For programs of > 100k gates, the time to execute a program can range from a few seconds to about a minute. For example, an AES 256 computation requires ~ 9k AND gates and 40k XOR gates.
Right now I would not use it for programs with more than a couple 100k gates, but the engine has not yet been optimized very much, at the moment the focus is on providing a good UX and an easy way for people to experiment with MPC. I'm pretty sure that with a bit of optimization efforts it will be possible to speed it up significantly.
That's only true for systems where the principle of explosion actually holds though, isn't it? So it wouldn't apply to paraconsistent systems.
In the end, Gödel is actually giving us a choice: Either accept incompleteness or accept inconsistency. Of course it's true that historically incompleteness has been perceived as the only viable choice, but at least a few paraconsistent logicians like Graham Priest have argued for (non-explosive) inconsistency instead.
Assuming that "crypto" was meant to refer only to cryptocurrency, there are a few companies working on non-blockchain/non-cryptocurrency crypto(graphic) tech which are paying as much as web dev jobs.
For example, I stumbled upon ockam.io during my last job search (no affiliation, and never interviewed with them as they weren't actively hiring when I wrote to them last year). I vaguely remember there being a few others, though I can't remember any names off the top of my head (it has definitely gotten harder searching for those kinds of companies as most job ads are drowned out by all the blockchain jobs). Old job posts on https://this-week-in-rust.org/ often contain a few interesting companies.
(Shameless plug: If anyone is interested in working at a non-profit focusing on non-blockchain cryptography in the field of multi-party computation, the company I'm working at is hiring at the moment and the salary ranges [for a 4-day work week] are listed: https://sinefoundation.notion.site/SINE-Job-Board-d28eda00c5...)
Unfortunately the situation is bit complex for Ludwig Wittgenstein (who died in 1951 and whose works should enter the public domain in countries with death + 70 years copyright).
Wittgenstein only published the Tractatus during his lifetime (which will enter the public domain), but all of his later works were compiled and published posthumously (as the "Nachlass") by his literary executors, most importantly the Philosophical Investigations. At the moment, Trinity College Cambridge hold the copyright to most of the Nachlass and they have more or less publicly said that they do not consider the Nachlass to go out of copyright in 2022, as there seems to be an obscure exception in British copyright for posthumously published manuscripts that would extend the copyright duration to 2039 [0].
Of course British copyright law does not directly apply to the rest of the world, but I sadly do not expect to see many public domain editions from academics in the coming years, since most of them want to stay on good terms with Trinity College. Others would perhaps like to publish an edition, but are unsure about the copyright situation.
Are there any non-profit organisations that provide legal clarification in these rather complicated situations for individuals that want to publish new editions of these works? IANAL, so I would be reluctant to sink too much time into such a project if there is the chance that I might be sued into oblivion by Cambridge.
(The whole interview is actually quite nuanced on the question of whether math is discovered or invented and well worth a watch. There are also interviews with other mathematicians and physicists in the series, for example with Roger Penrose, but most other researchers seem to hold a rather dogmatic and platonist view, which is why I found Chaitin's perspective refreshing.)
Wow, I did not expect a reference to 'Synecdoche, New York' to crop up here on HN, even less in such a fitting context. For anyone else wondering what this is about, here is the scene from the film (the whole film is worth watching if you are into the sort of postmodern-surrealist stuff):
Caden Cotard : I wanted to ask you, how old are kids when they start to write?
Madeleine Gravis : Listen, there's an absolutely brilliant novel written by a four year old.
Caden Cotard : Really?
Madeleine Gravis : 'Little Winky" by Horace Azpiazu.
Caden Cotard : That's cute.
Madeleine Gravis : Hardly, Litty Winky is a virulent anti-Semite. The story follows his initiation into the klan, his immersion in the pornographic snuff industry, and his ultimate degradation at the hands of a black ex-convict named Eric Washington Jackson Jones Johnson...
Caden Cotard : -Written by a four year old?
Madeleine Gravis : -Jefferson.
Caden Cotard : Wow, written by a four year old.
Madeleine Gravis : Well Azpiazu killed himself when he was five.
There are still nights I wake up screaming, remembering the time I tried to build an editor with contentEditable. Is there a special place in hell for those who forced this spawn of Cthulhu upon us? Or should we pity these souls, who were the first to lay eyes on these unimaginable horrors?
If you ever meet someone who thinks that the lovecraftian amalgamation of HTML/JS/CSS is a sane platform for developing applications, just tell them to build an editor using only contentEditable and the standard browser APIs. Then wait a few days. They will hate you, but at least they'll be forever cured of their delusion.
Yes, it's that bad. No matter how long you have been programming, no matter what you have built before, contentEditable will defeat you. Decades of experience, written your own programming language, database, editor? Oh you poor soul, contentEditable will laugh in your face, because there is no logic to it. It is the very embodiment of edge cases built upon edge cases, with a smidge of browser incompatibilities sprinkled on top, then all dumped onto the garbage dump that is caret handling.
I'm a contentEditable survivor. The dark episode is now behind me, yet no matter how much time passes, I will forever be scarred by the experience.
That's an interesting thought experiment, though I'm not sure how using "sounds of the appropriate length" or "lines of proportional length" would get you more than the rational numbers, which are already countable and thus fully captured by any Turing-complete language. To say that there are inexpressible real numbers is to say that there are numbers that are not rational but which can never be practically used or accessed either, at which point they become kind of like an invisible and unnoticeable unicorn: it is certainly possible to believe in its existence, but such a belief is quite different from the belief in the existence of practically useful real numbers such as pi.
I am not trying to convince anyone that inexpressible real number do or do not exist, but I think it's worth noting that these issues quickly cross over into the realm of philosophy, where it's not possible to justify a particular conviction by appealing to firm mathematical or practical reasons. Nothing wrong with that, of course.
Personally, I'm content with what is expressible in language and I consider mathematical concepts going beyond this boundary of expressivity as inessential to my own personal use, though I can certainly see that these mathematical calculi can be of interest to mathematicians on their own.
Oh, I see what the issue is. I wrote "smallest to largest and lexicographically", meaning first from smallest to largest (as measured by the length of the string) and then within each group lexicographically, which is the usual way of giving an enumeration of such expressions as far as I know. Of course you cannot enumerate these expressions if you expect a solely lexicographical ordering. In any case, English was just an example, you can basically pick any Turing-complete language that is recursively enumerable and count its expressions by considering its bit string encodings as natural numbers.
Edit: This is also why the computable numbers are countable, but not computably enumerable (because figuring out which expressions correspond to real numbers is equivalent to the halting problem).
EDIT: The parent first said (before being edited, with my original answer after the quote):
> Humor me and count out the first two real numbers in English in lexicographical order.
Probably "one" and "six" (then "ten" and "two", followed by all 4-letter expressions of real numbers), unless you can think of an English expression with a length of three letters or less that would occur before "one" and "six" lexicographically. If you consider "pi" or "e" to be descriptions of real numbers then clearly these would occur before "one" and "six".
But of course you can also pick an arbitrary universal Turing machine or other suitable formalism, pick an encoding as bit strings and order expressions in such a formal language according to their bit strings. Ordering expressions in the English language is only the less formal counterpart.
(If your point is that ordering expressions of real numbers in English is far from unambiguous without first agreeing on a dictionary of valid words and on rules of what can be considered an expression of a real number in more than one word then of course I would agree. But what I'm driving at is not that it's easy to unambiguously count out the real numbers in English, of course it's not, but rather that any kind of natural or formal language expressions, by being recursively enumerable, are "numerous" enough to be a countable set of expressions. To say that the real numbers are uncountable is to accept the view that there are real numbers that are not and can never be expressible in language, which is a view that only makes sense against the backdrop of a very specific philosophical framework. One that is definitely accepted more or less implicitly by most working mathematicians, but not the only possible one. And this philosophical framework cannot itself be justified or grounded by a mathematical argument such as Cantor's diagonal proof.)
---
Reply to the parent after edit:
> You could say the same about just real numbers, which can also be ordered from smallest to largest. This definitely not 'trivially' implies countability.
No, what I meant was that by ordering expressions in the English language or other suitable formal languages first from smallest string to largest string and within these groups lexicographically, you can enumerate all the expressions in such a language, which makes them trivially countable.
Of course this does not give you a 1:1 mapping from expressions in a language to real numbers, but it is meant to illustrate that the real numbers are not uncountable because they are 'too numerous' to be counted by the natural numbers, in the sense that a box is not large enough to hold a collection of things. They are uncountable because we accept the view that there can be real numbers that are not and cannot be expressible in language, which is a platonist view that is open to philosophical critique.
> In such a sense then, we can trivially "count" the real numbers unless we hold the philosophical view that there are real numbers that are not expressible. This is where it becomes a question of philosophy of mathematics, not mathematics proper.
I'm not disagreeing with your interpretation of Cantor's diagonal proof, I'm merely pointing out that this interpretation depends on a very specific philosophical view of mathematics, namely the platonist view that the real numbers exist independently from their expressions in any natural or formal language and that it makes sense to say that there are real numbers that are not expressible.
And yeah, nearly all working mathematicians will agree with this view and from their perspective the real numbers are uncountable, period, and you are right that what I sketched "doesn't work".
But I think it's important to remember that there are or could be alternative philosophical views of mathematics that lead to a different interpretation, which will reject not the mathematical validity of Cantor's diagonal proof, but rather its usefulness or relevance. After all, how can you convince someone that there are real numbers that are not expressible? By their very nature they cannot be practically used in any calculation, so how could you convince someone who is not convinced by this philosophical assumption of Cantor's diagonal proof?
In other words, Cantor's diagonal proof cannot prove that there are real numbers that are not expressible, because the proof only makes (philosophical) sense if you accept this viewpoint in the first place.
That depends on what you mean by "assigns uniquely", "rule" and "doesn't work", which is why this question is deeply entangled with philosophical issues that cannot be settled purely mathematically.
It is obvious that all expressions in the English language can be ordered from smallest to largest and lexicographically, which makes these expressions trivially countable. We can thus assign natural numbers to real numbers by assigning numbers to their expressions in a natural or formal language, which will of course include infinitely many expressions that are just nonsense descriptions and infinitely many expressions that map to the same real number. These expressions will also include any possible expressions of Cantor's or other diagonalized numbers. In such a sense then, we can trivially "count" the real numbers unless we hold the philosophical view that there are real numbers that are not expressible. This is where it becomes a question of philosophy of mathematics, not mathematics proper.
You can of course object that what you meant by "assigns uniquely" is an unambiguous 1:1 mapping and that including any number of nonsense descriptions misses the point. In that case giving a "rule doesn't work" because the diagonalized number always escapes the proposed system of counting the numbers, but only because the diagonalized number is allowed to 'parasitically' depend on the totality of the system, but is excluded from the system (or else it would diagonalize itself and become ambiguous at that particular decimal place). This particular viewpoint is tied to a particular philosophical position, however, and not all positions in the philosophy of mathematics will agree with it.
This all might seem trivial or even nonsensical (as philosophy of mathematics so often appears), but I merely want to point out that the 'uncountability' of the real numbers is not a consequence of the set of the natural numbers being 'too small' to hold all the real numbers, because they are 'large enough' to assign numbers to all possible descriptions all real numbers that will ever be expressed in language. Uncountability is a consequence of a view that restricts Cantor's diagonalized number from the set of the countable number but still considers this diagonalized number to be a real number (which again is only unambiguously defined if it is not allowed to diagonalize itself). There are however other possible philosophical viewpoints which either include the diagonalized number in the set of countable numbers (at the cost of including ambiguous or paradoxical numbers) or reject the view that Cantor's diagonalized number should be considered to be a real number in the first place.
tl;dr: Yeah, you can always name a real number for which a particular counting rule does not work, but only as long as there is agreement regarding the philosophical underpinnings. Most mathematicians can probably be considered platonists and from their standpoint the real numbers are obviously uncountable, but that is by no means true for all positions in the philosophy of mathematics.
Very, very impressive. I just spent the last hour going down the rabbit hole of reading your blog and browsing through your different side projects (which I can only recommend to fellow HN readers, the programming language posted here really is just the tip of the iceberg). Creating your own programming language is remarkable in its own right, but then using it to build your own frontend & backend frameworks, search engine, productivity suite, 3D renderer and a bunch of other apps ist just impressive on another level.
What I find most fascinating about your side projects is how you bring together a number of different skills in a way that looks almost effortless. Knocking out a search engine or a twitter reader as a throwaway learning project is one thing, but doing it over the course of little more than a week with a well designed UI in a way that ends up being useful in your own workflows? That not only takes some serious work but also the ability to correctly judge which directions not to go in, which can be one of the hardest aspects of developing software.
Here's another take by Wittgenstein from the preface of the Philosophical Remarks:
"This book is written for such men as are in sympathy with its spirit. This spirit is different from the one which informs the vast stream of European and American civilization in which all of us stand. That spirit expresses itself in an onwards movement, in building ever larger and more complicated structures; the other in striving after clarity and perspicuity in no matter what structure. The first tries to grasp the world by way of its periphery -- in its variety; the second at its centre -- in its essence. And so the first adds one construction to another, moving on and up, as it were, from one stage to the next, while the other remains where it is and what it tries to grasp is always the same."
I can't help but feel that this description of the "vast stream" captures the current trend in most of software development and academia quite well...
You are of course free to believe in mathematical Platonism, but that doesn't mean that non-Platonists would agree that proofs amount to objective "facts" about reality. And you are equally free to "prove it for yourself", which will just end up begging the question unless you are a Platonist.
That's not to say that math is subjective. But claiming that math is producing objective facts ignores at least a few hundred years of philosophy of mathematics (if not more). Even practicing mathematicians like Chaitin have described math as being more about inventing than discovering.
Holding a non-Platonist position also doesn't immediately lead to the sort of constructivist / "anything goes" position that some people ascribe to it, where you'd suddenly lose the ability to say that 2 + 2 = 4 and not 5. There are lots of philosophical positions that would agree that 2 + 2 is 4 without also claiming that this makes it a "fact" about any sort of objective reality or Platonic discovery.