skoodge

Just wanted to say that I personally enjoyed the little inconsistencies. It feels satisfying to discover interactions that I didn't expect, disorienting but in a good way.

> 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?

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.