There are many ways to embed sets in a type theory. For example, in a type theory such as Coq, one typically models sets as functions ‘T -> Prop’. This makes sets intensional too. For extensional sets, i.e. for which ‘forall S T, (forall x, S x = T x) -> S = T’, one needs additional axioms.
For an introduction to discrete mathematics it also makes sense to understand when a type is ‘discrete’: it must have a decidable equality. Intuitively, this means one can recognize whether any two elements of the type are identical. Often one also works with countable types for which one assumes it is possible to enumerate all its elements. The inductive data types one typically needs are all discrete and countable.
Interesting work in this direction: https://www.ps.uni-saarland.de/Publications/documents/ForsterEtAl_2019_VerifiedTMs.pdf
Reminds me of a draft spec for Invisible XML: https://homepages.cwi.nl/~steven/ixml/ixml-specification.html
So they’re looking to replace BSD/POSIX socket API with something else. Outright this sounds bad because it would mean all software need to be patched afterwards.
There’s more on Reo coordination language. Then there’s the api.
It looks like interesting and I’ll perhaps read more into this later. It actually kind of looks like it’d make sense.
A compatibility layer for applications using the socket API can use connectors underneath. But then the application cannot use the benefits of connectors, such as connecting with multiple peers and gathering session information.
About ten years ago, when I was still active on StackOverflow, I raised a similar question: https://stackoverflow.com/questions/2760794/x86-cmp-instruction-difference
Turns out someone then commented that these bits of freedom can be used to fingerprint executables: “These 1-bit degrees of freedom also provide a covert channel for compilers to “phone home” - they can “watermark” the binaries they produce, and the compiler vendor can ask you to please explain if they find your software with their watermark, but with no license on file.” – Bernd Jendrissek
Nice to still see interest in this stuff!
Thanks for asking that question. oddly enough, I was wondering about this topic a few days ago. I knew about the dual encodings, but I was wondering if disassemblers ever differentiated the mnemonic. I happened upon your stack overflow question.
It turns out that Nasm etc. do not differentiate. However, gas does and one of the answers to your question showed the .s suffix modifier. This was a nice fine since I couldn’t find anything in my normal Google searches.
There used to be an excellent shareware assembler named a86 back in the DOS days at a time when I actually wrote assembler. That used this technique for fingerprinting. I remember hearing that a number of viruses were found to have been assembled with a86.
I remember working for a client, who was still running critical business infrastructure, a DOS program from 1987. The request was to be able to upgrade to Windows 10 and have network printing working. An older set-up with multiple machines that ran Windows 98 and XP also allowed this, but the older machines were no longer available on the market and could thus no longer be replaced if they failed.
vDos allowed me to work with these requirement and is able to run the 33-year old binary without any change, fully featured, and now allows network printing but also network storage drives! I also submitted some patches back to Jos Schaars (but I don’t know whether they were useful to him). In general, I am quite positive about vDos!
Although, there is some weird blob (binary large object) in the source code that you obtain via e-mail by donating any amount via PayPal (to avoid dealing with non-serious users): I never really understood what functionality was implemented in that closed source blob.
I don’t get it. If there’s a problem with a library, why not fix it and upstream it? Most library authors are super happy about getting a pull request that improves things.
I have not have had a single PR denied that I opened on libraries and even opinionated frameworks to fix stuff or add small features. I’m just a single data point of course.
So let’s assume a case where submitting a fix does not work out: one can always fall back to reinventing the wheel in one’s code base, as suggested by the article. And I’ve seen plenty of that, but please, just stop. Chances are good that my homebrewed code will be much worse than any specialized library. And I know the same is true for the code of my coworkers. If anything, we need to stop reinventing the wheel so much and reuse and support more of the open source code out there, we would all be better off.
Reasoning linked in the article.
For the record, the argument is that certain communities are so toxic/annoying/irresponsible/whatever, that getting your patch accepted is difficult and you’d rather not deal with them. But it’s typically hard to replace a dependency further down a tree by your own (fixed) version. If important, one could keep a private fork of the dependency tree instead. And possibly share patches of that private fork amongst other intimi (Fight Club-style). But this does not directly contribute to the public community.
My own opinion is along similar lines: the social signalling function (e.g. think of employment prospects by showing personal contributions to open source projects) could compromise quality on the long run. The original post complaints about potholes, but this might also be influenced by the social signalling function. As people are motivated to publish and promote their code (potentially by getting awarded social status, as is gameified by social networks such as GitHub), the issue of quality may be of lesser concern. And as long as the quality of software remains low, a piece of software will not be (re)used in the long run.
Having a hard time to follow this argument, probably because I’m lacking the context. I understand the argument that there are certain communities one would want to avoid. If the majority of software in a chosen ecosystem are created by such communities, I feel sorry for that person, but can assure that there are more positive/fun/professional ecosystems out there, and hope that they have one day the opportunity to be part of one of those.
If there’s a problem with a library, why not fix it and upstream it?
Time. One reason why people use libraries and frameworks in the first place is so that they don’t have to understand a specific area: they can delegate that task to a (hopefully competent) third party. To study the library source code, find the problem, develop a solution, tidy up the solution, ensure that the solution works for all possible use cases supported by the library not just you own use case, and submit the fix, can take considerably more time than a quick bodge along the lines of “if it fails try again” or “if it fails, carry on regardless”. Many workplaces still don’t allow their engineers the time required to fix things properly and upstream the fixes.
TimSort is non trivial! Python and Java implementations of TimSort were for some time incorrect, but I believe this had been fixed. A detailed post that describes this is here: http://www.envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/
“The Tree Conjecture” is false. There are structures which cannot be represented as trees. If one accepts that anything representable as a finite string (including trees in this format) can be encoded as a natural number; and there are real numbers that cannot be enumerated; and structures might include those, then there are structures not representable as a tree.
Gödel’s incompleteness proof corresponds to Cantor’s diagonalization proof corresponds to Turing’s halting problem. The argument that for a proof system of arithmetic, there exists some true statement (using Gödel numbering) about natural numbers that is not in the theory, corresponds to the existence of a diagonal of numbers (flipping a digit) that is not tabulated in Cantor’s argument, corresponds to the existence of a machine (solving the Halting problem) that can not be decided. In the second case, we already accept that a larger class exists, known as the real numbers. In the first and last case, there must be a larger class of proof systems or machines: in fact, other (higher-order) proof systems exists, in an infinite (arithmetical) hierarchy: the consistency of one is provable in a larger class. For Turing machines, there can be larger machine classes, so-called real computing: these are not physically possible within finite space. My working hypothesis is that true concurrency already brings more than Turing computabily: P = NP assuming a polynomial number (in input size) of concurrently synchronizing computers. By the wat, Gödel numbering, that is encoding formal systems as natural numbers, is an idea going back to Leibniz where attention was drawn towards so-called characteristic numbers.
I believe null values are essential. Consider the following Java class, for which null is prohibited:
class Weird { Weird x; }
What would the value of x be, if it were not null? Clearly, it must be an inhabitant. Thus, every reference type has also null as inhabitant, to allow these cyclic definitions.
Suppose, you get rid of null and instead declare a particular global variable that is the “default” instance. Then, consider this:
class Weird2 { Weird2(Weird2 x) {} } default Weird2 = ???
How do you construct such a default value, if the constructor takes an instance as reference? That would only be possible if you consider object references for which constructors are not completed. That might give you an even bigger mess than null.
In any case, dealing with cyclic structures is not easy. If not null, there must be other trade-offs to be made, such as uninitialized objects.
I very well understand what you mean. However, if you introduce null for this reason then you cannot use your types to prove that you have completely instantiated structures that behave properly.
Though in Java you already have other features that ensure types do not have the meaning they should hold. This was the reason why I advised to not bother if the language already has null in it.
Oh, in Java you can observe fields that haven’t been assigned yet (even final fields!). Weird! Given that, maybe null is essential in Java.
Some languages don’t really have constructors in the Java sense. To create an instance, you have to supply an initial value for each field before you get back a reference to the new instance. This means you never have uninitialized fields, but it also means creating cycles is more difficult. (That can be nice though: you can look at a type and immediately know there are no cycles.)
If you wanted to design a language without null, but with Java-style constructors, maybe you could add more restrictions. For example, maybe the constructor has to call super and initialize every field before it’s allowed to refer to this
.
For those who do not know: TenCent is Chinas Amazon and Google. See https://en.m.wikipedia.org/wiki/Tencent
Long term: datacenters move to outerspace for simple reasons, 1. superconductivity allows raising clock speeds to around 700Ghz, 2. distance to geostationary orbits is rougly equivalent to distance to nearest datacenter, 3. lifting matter into orbital space becomes faster and cheaper, 4. near absolute zero temperature is cheaper to keep computers cool in, compared to typical temperatures near earths surface, 5. energy is provided by nuclear reactor, since less environmental problems, 6. larger elliptical orbits are used for non-realtime computations, effectively filling space: shadowing the sun on earths surface controls global temperatures.
When we speak of the “cloud,” the next generation will point upwards into the sky. And for good reasons.
Dumping heat in outer space is actually really hard – where do you put the heat?
Data centers submerged in oceans would be a far likely scenario.
Current satellites vent heat via radiation, right? Maybe it wouldn’t be practical at “DC scale”, but I feel like with a big enough surface area (?) you could radiate heat out into space, assuming that you don’t mind being lit up like an IR beacon :-)
Point 1 prevents generating heat, otherwise you loose superconductivity. Therefore, computations are most of the time reversible, eliminating the generation of heat in the first place.
“The project seems to have died in 1996…” https://en.wikipedia.org/wiki/QED_manifesto
The following I could find as a critical evaluation of the QED manifesto: http://mizar.org/trybulec65/8.pdf
But that it died in 1996 is by no means established.
In fact, European/national research moneys are still to this day granted for development that lies within the scope of the QED manifesto. For example, https://lean-forward.github.io
Coincidentally, the author of the critique participates in this latest project.
One of the best talks I have recently seen. Thank you! What this inspires in me is:
Take seriously what people believe, but explain when and what makes it true, and when and what makes it false. Your citrus-analogy is almost as powerful as Dijkstra’s sterile analogy [EWD1054]. Taking this highly critical stance, then allows you to separate deeply ingrained ideas (by “internet advice gurus”) into clear and meaningful concepts.
We need more and clear material for understanding principles. Your presentation did not provide much details into the state of the art (rightfully so), but neither gives any concrete pointers to the audience on how to proceed with the paths you laid out.
However, the latter point I fail myself to provide. The pointers I have are very technical in nature and do not provide a good overview on principles per se. My own education consisted into collecting many different sources, which is a regrettable state of affairs of science of computing.
Agreed on both points. Collecting such material from various sources and explaining principles is much of the work I do in my blog and my business.
I haven’t deeply researched the history of project methodologies, but I’d be unsurprised if the belief that “all we did was waterfall until Agile came along” isn’t true. Pretty much every OOP book I’ve read from like 1980-1995 talks about how it works with an “Incremental model”, where you deliver short term wins continuously and constantly reevaluate customer requirements.
You might find this thread helpful. Turns out iterative development was the norm, waterfall was an illustration of what wasn’t done, and one guy used that to con folks for money on top of DOD’s top-down management. Then, the world changed for the worst. That’s the story so far.
Nothing I’ve read from programming books since the 1970s suggests that Waterfall was “the way” that software was developed. I’ve also not researched this deeply, but I don’t think Waterfall was ever taken seriously. Everything I read talks about the importance of testing intertwined with implementation, in some form, when developing software. Furthermore, there was always talk of iteration to get APIs to be better. The key difference from the early days is that those cycles were longer, which gives the appearance of Waterfall in action.
I think our understanding of classical engineering is partially shaped by the agile industrial complex.
Nowadays if you attend a Scrum training somewhere you get a trainer who typically never worked in a classical engineering project. Yet they have learned the story that classical engineering was waterfall and that no project was succesful ever and that every developer suffered. So they perpetuate this story. Since they don’t know stuff, they just randomly talk about waterfall/classical methods/v-model as if they were all the same. This portrayal of classical methods has shaped our mental model so much, that it also shaped how classical engineering is implemented.
I have an older colleague who always dies a little every time a 30-something agile consultant starts lecturing people on the perils of classical engineering and the gospel of agility. “If the V-Model was waterfall, it would be the ’'-Model”.
Bertrand Meyers article I also found interesting on this http://se.ethz.ch/~meyer/publications/methodology/agile_software.pdf . Especially his defense of requirements documents IIRC.
Maybe this is a general thing to remark about adoption of ideas here. It is always a good idea to read and study the primary and early sources for ideas. Quite often, ideas deteriorate while they are adopted. Most material on user stories is a very shallow remainder of the ideas that Cohn wrote down in the 2000s in his book. The same goes for the original “waterfall paper”, the agile manifesto, even the scrum guide (ever realized it does not mention agile once, it does not mention story once?). I’d be actually curious about historic, alternative frameworks/processes that were created at the same time but that were not widely adopted and have silently vanished. I think a lot of wisdom could be found.
Do requirements documents need to be defended?
If you have no requirements document, how do you know when you’ve fulfilled your contractual obligations?
You probably don’t have contractual obligations. You’re probably building internal software and the requirements could change for those on some sprint-like basis. And that’s okay.
Essentially you just have a tight iteration loop and all is well.
Well, many agile consultants will tell you they are the devil and not agile. (They are not agile if you set requirements in stone at some point). When in fact, user stories (advocated as the alternative) are just a different flavour of requirement engineering.
Personally I think writing a large requirements document upfront might be a bit risky if you already fear that your project is based on risky assumptions. On the other hand in the Scrum-hamster wheel, it is sometimes hard for the team and the PO to think for a bit and come up with a better solution than the lowest hanging fruit.
I have bad experience with requirements documents when customers commissioned software development, because often they were too detailed and kind of outlined problems the user didn’t have. Then I would have favoured a more agile approach.
In SaaS contexts, I would have loved to have a well-maintained requirements document at times, especially when parts of the system were rewritten or exchanged
From the picture of the process of Agile in the article, I see: Design, Develop, Test, Deploy. But where is verification? Poof, gone.
Typically I say that there are two kinds of validation (“does the software posses certain qualities?”): testing and verification. The former is established empirically (user tests, examples, etc.) the latter established mathematically (through proof and reasoning).
Testing essentially establishes that software has the intended functionality; after succesful testing, there should not be any confusion over what the software does, i.e. no misunderstanding over that the software provides certain functionality.
Verification essentially explores unknown consequences, not foreseen by testing. But only by rigorous argumentation, one can explore all possibilities in which problems may lie hidden. After succesful verification, there should not be any junk in the software, i.e. no unexpected behaviors.
Both phases provide essential information for clear and consise documentation.
Agile vs waterfal discussions seem to attack a strawman, while not providing any useful information to conmplete the verification phase.
Reuse works, but if it does it remains invisible and non-obvious. In the big: always write an OS, compiler, I/O routines, such as graphics or networking, from scratch? No? These “softwares” are very suitable to reuse. In the small: always write a custom data structure, and manipulation routines such as parsing, sorting, printing, for each different kind of object? No? The tiny objects that are sufficiently encapsulated can be treated generically, thus enabling reuse.
I have seen many argue that certain programming languages are discovered. I disagree. For the lambda calculus, Turing machines, and recursive functions, one uses as argument they are equivalent by mere chance, thus they are independent discoveries of the same “thing” that already exists “out there”.
This is false. Church, Gödel and Turing all worked at some point even at the same location. Consider that they could have exchanged ideas either directly or indirectly (through collegues).
The programmers of the Functional camp also easily fall into the trap, that algebraic data types, type classes and other features such as unification are “out there” to be “discovered”. The fact that these languages can be understood in a minimal calculus, only highlights a fundamental fact:
We are good at transmitting information about programming. Two people can learn and interpret information from two different sources, and still derive the “same” structure.
We could equally jubilate that “programming education” is so effective, since so many people are drawn out to see the same “light”.
Maybe this is the case, maybe not. There are some very interesting connections. I apologize in advance for category theory.
First, the category Set, whose objects are sets and arrows are functions, is also a topos. In fact it is the simplest topos, in a sense; Set can be built by considering all of the different ways to examine a point as a topological space.
Every topos is Cartesian closed, which means that it has actions which resemble currying and application. Indeed, every topos has an internal logic, and there is a famous isomorphism, the Curry-Howard correspondence, which connects this logic to an internal language. Every Cartesian closed category has an internal language that looks like typed lambda calculus, and thus, so does every topos. This connection is sometimes called the Curry-Howard-Lambek correspondence.
Now, having laid out the foundations, you can consider this listing of examples of the correspondence.
To address your points more directly: It is true that Church, Gödel, and Turing were all on very similar paths. Gödel and Turing, along with Nash, also had hinted at describing the basics of modern complexity theory, talking about what would become P and NP. Support for the Church-Turing thesis comes, to me, from Turing-complete systems being shown to be Turing-equivalent (so far), and from metalogical results like those of not just Gödel and Tarski, but also more modern progress in constructive mathematics, where it is not false that all real numbers are computable and all computable functions are continuous, just like in Turing’s model.
Algebraic data types, as the name implies, arise from algebras on types, like in the typedefs mini-language. They are not limited to “functional” programmers; Zephyr ASDL is used by (my language) Monte, Python, Oil, and probably others.
Some type classes naturally arise, in the sense that we can imagine topoi where class-like features would be granted automatically to all computations, without changing the underlying logic. This is possible because logic is portable between topoi. In particular, the Haskell typeclass Ord
corresponds to every type having a free (partial) order, and Eq
to equality; we could give both for free by working in a topos like Pos, the category of partially-ordered sets; logic in this topos is the same as in Set, but richer in the values.
Unification arises in a beautiful way, to me. In Rel, the category whose objects are sets like Set, but whose arrows are relations, the directions of arrows do not matter much. If we bend all of the arrows to one side, then the unifications bulge out on the other, and computation in Rel can consist entirely of first bending the arrows (choosing which values are inputs and which are outputs) and then reducing the diagram piece-by-piece and checking each unification as it bulges out.
What I find entirely fascinating is that, according to the categorical logic, there should be at least one more family of logics besides the Cartesian-closed (“functional”) and monoidal-closed (“relational”, “logic”) languages, corresponding to weaker closure, and there is: linear logic! Linear logic is being explored right now in PLD and PLT circles, and its relevance was predicted by the mathematical framework.
Your description of unification via Rel is fascinating. What should I read to understand it better?
There is a paper, Knowledge Representation in Bicategories of Relations, which has diagrams that depict relations in a visceral way. I usually imagine a pure logical language, too, like µKanren, which can be viewed as an internal language for the categorical diagrams.
I apologize for not having a page with images which show exactly what I described. I started work once on a writeup of how µKanren or other pure logical languages relate to relational categories, via the relatively obvious functor which sends diagrams to µKanren programs, but didn’t think that there would be much interest.
Even without collaboration, the combination of consistency and minimalism that acts as the fitness function for mathematical discovery is a pretty intense constraint, so it should be unsurprising that lots of the things we invent under those constraints are equivalent.
If you’ve got an urn with ten thousand green balls, one hundred light-blue balls, and two dark-blue balls, and we’ve got a rule that we only pick blue balls, we shouldn’t be surprised that a lot of the ones we pick are light blue – because we’ve made the green balls irrelevant to the selection. In the same way, if from the problem space of mathematical ideas we only choose consistent and minimal sets of ideas, and most forms of consistent minimality have certain attributes in common, we shouldn’t be surprised that we keep choosing ideas with those attributes – the majority of potential mathematical ideas are irrelevant to our selection purposes, and the rest are biased in particular ways.
The languages people claim are ‘discovered’ are merely very internally consistent. Consistency is valuable in of itself, because it makes predicting new behaviors based on knowledge of a priori rules easy. But, consistency is enough to vastly increase the likelihood of overlap with other consistent systems (like… all of mathematics).
This is basically my position on the topic.
I can’t justify platonism, it doesn’t seem sensible to me. But I do think if we solve similar problems while filtering for simplicity then we’re likely to solve them in similar ways.
Other than lambda calculus, Turing machines and recursive functions being equivalent, what is also very important is that since then no non-equivalent alternative has been found. You can’t blame that on everyone having exchanged ideas: all kinds of mathematical inventions/discoveries were found by people whose coworkers actually disliked and disagreed with their conclusions as long as possible. The invention/discovery of complex numbers, quaternions, Gödel’s uncertainty principles, cardinal numbers due to Cantor’s diagonalization argument… the list is endless. It seems quite unlikely a non-equivalent alternative will still be found, independent of whether you consider it a discovery or an invention.
This is a great example to try to explain a mod practice because this post is right at the line for topicality, and really a little over the line into off-topic. Lobsters isn’t customer support for popular services, and is not the torch and pitchfork outlet. A post from the person who designed this system would be much better. But this link most likely will just prompt an thoughtful discussion about a small security design issue (that’s novel, at least to me and comments so far) and seems very unlikely to turn into a flamefest or brigade mob, so I’m OK leaving it.
Thanks for pointing this out! Bit of context: I was myself very surprised to learn of this feature, as I had never heard of it before. There was a mysterious issue with a colleague of mine, who said he could log-in using his phone but not with his desktop machine on a Gmail account. The phone had the password stored in its keychain, and when unmasking the password field we saw it clearly: it worked for signing in. Typing it over then resulted in an error on the desktop. We were baffled! Could not find a better source of it than this discussion, but wanted to share the “thing” here on Lobsters.