I have investigated this sentence: “The first author’s analysis of political metaphors in the Java libraries (Blackwell 2006) has already drawn attention to the fact that social and political concerns may be central to future research in the psychology of programming.”
There is a confusion in reference, but (2006a) “Metaphors we program by: Space, action and society in Java.“ was a very interesting read. It did not conclude anything on politics, but did a literal corpus analysis of Javadoc texts. Many surprising concepts were revealed, but suggestions or convincing explanation lacking. Examples:
I really appreciate that the misuse of “enumeration” is pointed out. See previous thread:
https://lobste.rs/s/ach1fc/openssh_username_enumeration#c_4gcwqw
The idea of enumeration, in my mind, seems to mean: emumerate all possibilities and filter out if some element is not valid. This results in an enumeration of all valid elements.
Some might interpret it to mean: enumerate only valid elements. This is equivalent. Consider the extreme case: if there are no valid usernames (i.e. fake SSH servers that disallow any username) then the method still enumerates all possibilities but never finds out any true username. Vacously, this enumerates all valid usernames.
I don’t really think that you should be allowed to ask the users the sign a new EULA for security patches. You fucked up. People are being damaged by your fuck up and you should not use that as leverage to make the users do what you want so they can stop your fuck up from damaging them further.
Patches only count if they come with the same EULA as the original hardware/software/product.
Sure - you’re welcome to refuse the EULA and take your processor back to the retailer, claiming it is faulty. When they refuse, file a claim in court.
Freedom!
This suggestion reminds me of the historical floating point division bug. See https://en.m.wikipedia.org/wiki/Pentium_FDIV_bug
There was a debate about the mishandling by Intel. Also, there was debate over “real-world impact,” estimates were all over the charts.
Here, it seems that the impact is SO big, that almost any user of the chip can demonstrate significant performance loss. This might become even bigger than the FDIV bug.
They are being sued by over 30 groups (find “Litigation related to Security Vulnerabilities”). It already is.
As of February 15, 2018, 30 customer class action lawsuits and two securities class action lawsuits have been filed. The customer class action plaintiffs, who purport to represent various classes of end users of our products, generally claim to have been harmed by Intel’s actions and/or omissions in connection with the security vulnerabilities and assert a variety of common law and statutory claims seeking monetary damages and equitable relief. The securities class action plaintiffs, who purport to represent classes of acquirers of Intel stock between July 27, 2017 and January 4, 2018, generally allege that Intel and certain officers violated securities laws by making statements about Intel’s products and internal controls that were revealed to be false or misleading by the disclosure of the security vulnerabilities […]
As for replacing defective processors, I’d be shocked. They can handwave enough away with their microcode updates because the source is not publicly auditable.
The defense could try to get the people who are discovering these vulnerabilities in on the process to review the fixes. They’d probably have to do it under some kind of NDA which itself might be negotiable given a court is involved. Otherwise, someone who is not actively doing CPU breaks but did before can look at it. If it’s crap, they can say so citing independent evidence of why. If it’s not, they can say that, too. Best case is they even have an exploit for it to go with their claim.
I don’t really think that you should be allowed to ask the users the sign a new EULA for security patches.
A variation of this argument goes that security issues should be backported or patched without also including new features. It is not a new or resolved issue.
Patches only count if they come with the same EULA as the original hardware/software/product.
What is different here is that this microcode update also requires operating system patches and possibly firmware updates. Further not everyone considers the performance trade-off worth it: there are a class of users for whom this is not a security issue. Aggravating matters, there are OEMs that must be involved in order to patch or explicitly fail to patch this issue. Intel had to coordinate all of this, under embargo.
This reminds me of HP issuing a “security” update for printers that actually caused the printer to reject any third-party ink. Disgusting.
I had not considered the case where manufacturers and end-users have different and divergent security needs.
It’s worth thinking on more broadly since it’s the second-largest driver of insecurity. Demand being the first.
The easiest example is mobile phones. The revenue stream almost entirely comes from sales of new phones. So, they want to put their value proposition and efforts into the newest phones. They also want to keep costs as low as they can legally get away with. Securing older phones, even patching them, is an extra expense or just activity that doesn’t drive new phone sales. It might even slow them. So, they stop doing security updates on phones fairly quickly as extra incentive for people to buy new phones which helps CEO’s hit their goalposts in sales.
The earliest form I know of was software companies intentionally making broken software when they could spend a little more to make it better. Although I thought CTO’s were being suckers, Roger Schell (co-founder of INFOSEC) found out otherwise when meeting a diverse array of them under Black Forrest Group. When he evangelized high-assurance systems, the CTO’s told him they believed they’d never be able to buy them from the private sector even though they were interested in them. They elaborated that they believed computer manufacturers and software suppliers were intentionally keeping quality low to force them to buy support and future product releases. Put/leave bugs in on purpose now, get paid again later to take them out, and force new features in for lock-in.
They hit the nail on the head. Biggest examples being IBM, Microsoft, and Oracle. Companies are keeping defects in products in every unregulated sub-field of IT to this day. It should be default assumption with default mitigation being open API’s and data formats so one can switch vendors if encountering a malicious one.
EDIT: Come to think of it, the hosting industry does the same stuff. The sites, VPS’s, and dedi’s cost money to operate in a highly-competitive space. Assuming they aren’t loss-leaders, I bet profitability on the $5-10 VM’s might get down to nickles or quarters rather than dollars. There’s been products on market touting strong security like LynxSecure with Linux VM’s. The last time I saw price of separation kernels w/ networking and filesystems it was maybe $50,000. Some supplier might take that a year per organization just to get more business. They all heavily promote the stuff. Yet, almost all hosts use KVM or Xen. Aside from features, I bet the fact that they’re free with commoditized support and training factors into that a lot. Every dollar in initial profit you make on your VM’s or servers can further feed into the business’s growth or workers’ pay. Most hosts won’t pay even a few grand for a VMM with open solutions available, much less $50,000. They’ll also trade features against security like management advantages and ecosystem of popular solutions. I’m not saying any of this is bad choices given how demand side works: just that the business model incentivizes against security-focused solutions that currently exist.
I wrote a small paper for class on this, actually! https://bernsteinbear.com/dat-paper/
Good technical overview. Identifying WordPress (25% of WWW) as a potential for growth is an interesting suggestion.
Thanks! Glad you thought so. I figured it would be a good starting point since many WordPress blogs use minimal dynamic content that cannot be expressed as a static website.
Very interesting paper, especially the appendices on computing/recognizing by extending derivatives of regular languages, to derivatives of context-free languages. Afterwards, a comment was made regarding intersection types: context-free languages are not closed under intersection, but it is possible to add an intersection type to the type system: all their theorems remain true. This increases the expressivity of the grammar beyond that of context-free languages.
Gödel’s Theorem (aka Gödel’s First Theorem) says that any sufficiently powerful formal system is either incomplete or inconsistent — in essence, either it can’t prove everything that’s true, or it can prove things that aren’t true.
This is a conceptual mistake. For starters, the notion of “everything that’s true” isn’t well-defined. Are we talking about truth in a theory, or truth in some specific model?
As furia-krucha said in a comment, Gödel’s completeness theorem says that a statement in a first-order theory is provable (i.e. a theorem) iff it holds in every model of the theory. For example, if a statement in the language of groups is neither provable nor refutable, there exist groups where the statement holds, as well as groups where the statement doesn’t hold.
Gödel’s first incompleteness theorem then says that every effectively axiomatized first-order theory (i.e., whose theorems can be enumerated) contains statements that are neither provable nor refutable. It says nothing about the “actual truth” of said statements. They are true in some models, false in others. Heck, they remain neither provable nor refutable in some models!
Gödel’s first incompleteness theorem then says that every effectively axiomatized first-order theory (i.e., whose theorems can be enumerated) contains statements that are neither provable nor refutable. It says nothing about the “actual truth” of said statements. They are true in some models, false in others. Heck, they remain neither provable nor refutable in some models!
I am considering this: a theory is defined to be the set of statements that are provable by the axioms and deduction rules of said theory. So “a first-order theory contains statements that are neither provable nor refutable,” makes no sense to me.
What do you mean by “actual truth”? A theory is merely a language; within it we say things, which we are supposed to believe to be true. If a theory is unsound, then you can say something in the theory that is not “actually true”, and conversely if a theory is sound then every expression that can be proved must be “actually true”. So, a theory says at least something about “actual truth” of statements, namely that if we believe a theory to be sound then we believe every provable statement to be true.
Sometimes you have reasons to believe a theory to be unsound, namely if you can find one counter-example of a statement that is provable, but which you know to be false.
“Heck, they remain neither provable nor refutable in some models!” I don’t understand you here; how can you prove something in a model, if a model is just a way of expressing what is true, viz. a semantics? Models don’t necessarily have an associated proof theory; they are simply constructions which we believe characterize certain real-world elements. Only for sound and complete axiomatizations is it the case that we have that all models correspond to a statement in its (sound and complete) proof theory. But Gödel here argues that no such complete proof theory exists for sufficiently powerful axiomatizations.
Coming back to the original quote: “in essence, either it can’t prove everything that’s true, or it can prove things that aren’t true.”
I believe that this correct. I read “it can’t prove everything that’s true” as simply meaning “there exists something that is true which it cannot prove”, as a counter-example to the universal quantification, and to me that is incompleteness.
As his theorem is a basic diagonalization theorem, I expect this to be of equal value as: “a Turing machine either can’t prove that it halts, or it has incorrect proofs,” which is basically the Halting theorem: it is undecidable by a Turing machine whether some other Turing machine halts on a given input.
Do you agree or is this just nonsense?
I am considering this: a theory is defined to be the set of statements that are provable by the axioms and deduction rules of said theory. So “a first-order theory contains statements that are neither provable nor refutable,” makes no sense to me.
Errr, sorry. What I mean is: You have a theory T defined using a language L. If T is both consistent and sufficiently powerful, then L must contain statements that are neither provable nor refutable in T.
What do you mean by “actual truth”? A theory is merely a language; within it we say things, which we are supposed to believe to be true.
I’m not supposed to “believe” anything. I’m supposed to use it to prove things. If I’m given an inconsistent theory, I can prove contradictory statements, and that’s all there is to it.
If a theory is unsound, then you can say something in the theory that is not “actually true”, and conversely if a theory is sound then every expression that can be proved must be “actually true”.
I disagree with the notion of “actual truth” to begin with, at least as something mathematics should be concerned with. Provability offers a compelling, very concrete alternative, as it can be computably verified, if we are careful about how define our theories. Truth is best left to philosophers.
Models don’t necessarily have an associated proof theory; they are simply constructions which we believe characterize certain real-world elements.
Whether there exist models of mathematical theories “in the real world” doesn’t really concern me. For me, a model must itself be a mathematical object, for example, a group is a model of the theory of a group, and a category of group objects is a model of the theory of groups (as entities that interact with one another).
I believe that this correct. I read “it can’t prove everything that’s true” as simply meaning “there exists something that is true which it cannot prove”, as a counter-example to the universal quantification, and to me that is incompleteness.
Why do you assert that unprovable statements in a theory are true, if there exist models of the theory in which they are false?
I’m not supposed to “believe” anything. I’m supposed to use it to prove things. If I’m given an inconsistent theory, I can prove contradictory statements, and that’s all there is to it.
I agree with you, in principle. However, I also consider that it is in general undecidable whether a given first-order theory is consistent. Therefore, if you give me a random theory, I have no other choice than to believe.
Provability offers a compelling, very concrete alternative, as it can be computably verified, if we are careful about how define our theories. Truth is best left to philosophers.
Very good point; some logicians also prefer provability over truth. But we simply shift our focus here, from “that is true in the real-world” to “that can be computed in the real-world”, both of which are still left to philosophers: simply stated, computability still suffers from the assumption of the Church-Turing thesis.
What you say about verifiability, is also quite subtle: the “carefulness” in the definition of theories probably means that we need a decidable theory. Hence, theories not “sufficiently powerful”.
Sorry for my vague meaning, but with “real-world elements” I, indeed, also mean mathematical constructions. However, it also includes the objects for which mathematics not yet has adequate characterizations.
Why do you assert that unprovable statements in a theory are true, if there exist models of the theory in which they are false?
Not sure. What is a model of a theory? To me that sounds like a proof object. For example, groups are a model of group theory, and groups themselves are proof terms of said theory. If your definition of “truth” is exactly the same as your theory, then, indeed, you are right: in terms of programming it means “all its bugs are its features.”
But to me that feels not right: a theory is true until you encounter a sentence which it proves but to which you not agree. Similarly, Brouwer felt that “the law of excluded middle” is somehow not “actually true,” and started developing Constructive Logic. There are similar reasons for the existence of Linear Logic, which basically amounts to not believing that you can apply a certain term (think: proof of some lemma) indefinitely often.
I think another approach of viewing Gödel’s incompleteness theorem is as follows:
We know that certain languages, say Peano arithmetic, can “realize” certain theories. That means, within the axiomatic system of Peano arithmetic, we can encode a proof theory that expresses certain truths. This “embedding” is also known from constructive first-order logic, where we can perform double negation translation of any classical sentence and find a constructive sentence that is true if and only if the classical sentence is true.
Now consider a system that is self-embeddable, that is: we know that every statement can be encoded into the object-level of the language and we can prove that this is a correct realization. Now, if we analyse the statement something along the lines of a Liar paradox: “I am not provable”. If the statement is true and the system is complete, it means that there exists a proof. We now encode the proof into the object-level, i.e. by realizing the proof into the system itself, call this the number G. Then we construct a new statement: “G is not provable”. Clearly this is not true, since as counter-example we can point to the proof G itself. However, “I am not provable” is true, but “G is not provable” is false: contradiction, hence the system cannot be complete.
And this last paragraph is the “basic diagonalization” which I mentioned last time: feeding the system into itself. It is the same trick that is used by Cantor to show that the Reals are larger than the Rationals. If you think Gödel’s Incompleteness Theorem is false, then you must also believe that the Reals are equally large as the Rationals!
Therefore, if you give me a random theory, I have no other choice than to believe.
You don’t need to “believe” in a theory to use it.
But to me that feels not right: a theory is true until you encounter a sentence which it proves but to which you not agree.
It isn’t clear to me what you mean by a theory being “true”. For me, all that a theory can aspire to be is “useful”, and that ultimately depends on your purposes. Programming has uses for inconsistent theories (such as most type systems, when viewed as logics), and I wouldn’t be surprised if so did physics.
We know that certain languages, say Peano arithmetic, can “realize” certain theories. That means, within the axiomatic system of Peano arithmetic, we can encode a proof theory that expresses certain truths.
I’m aware. In fact, in my original comment, I was going to say something along the lines of “Arithmetic is very powerful. If mathematical induction is available to you, you can define more general inductive structures, such as the syntax and (proof-theoretic) semantics of first-order logic…”, but then I forgot how I was going to relate that to the original topic, so I dropped it.
If you think Gödel’s Incompleteness Theorem is false, then you must also believe that the Reals are equally large as the Rationals!
Of course, I don’t think Gödel’s incompleteness theorem is false. I just disagree that you can extract any conclusions about “truth” from it, because “truth” is extra-mathematical.
Why do you assert that unprovable statements in a theory are true, if there exist models of the theory in which they are false?
I see now what you mean, by “conceptual mistake”. By soundness and completeness, a statement is provable if and only if the statement is true in every model. If a statement is unprovable, there exists some model in which the statement is false. So it can not be the case that an unprovable statement is true.
I think both the author of the original post and I have mixed up the two notions of completeness here:
Just reading this topic from a while back. Thank you for this discussion, really wonderful to read back!
Thanks for this amazing project!
If I may, I’d like to gently complain about this sentence:
Provably correct code is code that you can totally guarantee does what you say it does.
Thinking about total guarantees in this way confused me about proving code for a long time. Whenever I saw a “proven” piece of software, I could immediately think of several possible ways for it to nevertheless be wrong, so it was unclear how the “proof” was qualitatively different from other verification strategies.
Maybe a more accurate description could be:
Provably correct code is code that has been rigorously shown to implement a thorough specification using proof techniques from mathematical and logical praxis.
Yeah, I’m against the use of word guarantee or anything absolute like that. It hurt the formal methods field in the past when they were overpromising. Maybe something like, “Provably correct code is mathematically-proven to implement its intended behavior. If the specification is correct, code built this way usually has few to no errors in practice.”
Something along those lines. Maybe even with a link to CompCert’s testing results or something like that to illustrate the point.
Correctness is a relation between the input and output of a program. We say a program is correct if for every possible input, an execution of the program eventually results in a termination with the expected output.
The correctness relation is called functional if for every input only a single output is related. That is, each input uniquely determines an output.
Not all correctness relations have a correct program. An input-output relation for which no correct program exists is called undecidable. On the other hand, some correctness relations have multiple correct programs.
Typically, a programming language itself is already a specification language that allows one to establish an input-output relation in a rigorous manner. Sometimes one wishes to give a functional/relational specification before implementing a program, typically written down using mathematical notation.
Recent tools allow us to express functional/relational specifications on the computer too:
This is, of course, a simplification. Typically, the system one wishes to formalize is not functional, and thus requires more effort in abstract specification and refinement.
The words “rigorous” and “thorough” are not needed.
There’s a difference between establishing all that in math and it actually being true for the real code. It requires your specification to be correct, any specs/logics it depends on, the proofs, the checker, usually a parser, usually some I/O, the hardware, and so on. In this case, some of them needed automated solvers to be correct that are pretty complicated. I’m no sure that all have witness certificates or whatever they’re called yet. To be fair to proof engineers, many of them mention all of the above in their papers in the section describing assumptions and/or the TCB.
So, mbrock’s point that calling it a guarantee is too much seems to stand. I mean, even the seL4 people didn’t call it a total guarantee. They said the code should follow the spec assuming (long list here) isn’t wrong or broken.
I agree with your points. A proof is as much worth as you want it to be. See the DeepSpec project which tries to obtain proofs for a pragmatic computer: hardware specifications, OS specifications, prover specifications et cetera. However, this still not guarantees anything absolute.
My point is still that “Rigorously shown:” is vague. When is a method that shows correctness rigorous, when is it not? “Thorough specification:” is vague. When is a specification thorough, when not? Both are matters of trust, it seems to me.
“But there is a difference between showing that in math and it really being true for code.” Well, if one mathematically deduces a property of some code, and it turns out to be really false, one should start to doubt the foundations or mechanism by which the deduction took place. In principle, any deduction should be true for the real code.
Although in some logics, not all true properties can be deduced (incompleteness), it does not mean that we should accept logics in which false properties can be deduced (unsoundness).
Or did I misunderstand what you mean by “the real code”?
“My point is still that “Rigorously shown:” is vague”
Ok. That’s a decent point. It is kind of vague. It does have a subjective meaning that a lot of people already understand. They think that a “rigorous” analysis, testing, or whatever phase means piles of effort was put in vs a non-rigorous approach. They expect to get significantly more results or less problems. The fact that people rarely use that word for software QA might make that perception sink in even more.
I think I mainly keep using it for the psychological impact on people that might not understand the formal terminology well. I could tell them it relates to the specification. Yet, they might think UML when I say that. So, personally, I use a mix of precise terms from the field and terms that seem to convey understanding to those outside of it. I have no proof this term is better: by all means experiment to see if it works in your conversations or find a better way to say it. Talking rigorous vs typical QA has just worked for me. From there, I might say low, medium, or high rigor, confidence, and so on. Although the field is called assurance, I’m thinking of ditching that word, too, since confidence clicks in more people’s heads. I’ve been seeing some people talking about “high-confidence” software or techniques that “increase confidence that software works as intended.” Robustness and resilience are the other two terms many are using.
The message posted about how the sign-up page contains a bug was the reason I also tried to sign up. After three times and being warped back to the homepage, I gave up. How ironic.
When the author mentions OO:
There’s a very specific poor design at the core of the whole, well, not concept in the abstract, but ideology as practiced.
I can’t resist myself to refuse the notion of OO ideology. What does ideology even mean here? Let me guess:
If one tries to understand the theory behind OO, and fails, and applies some of the ideas in an apparant chaotic way that resemblences it.
But this, in my opinion, happens with most things one tries to learn. No blaim to the student, for he is only interested in learning more!
Let me close with a poem:
Object-orientation without subclasses is like functions without arguments.
Inheritance is not important for OO programming at all. It’s about substitutability, and if done the way it was originally intended, message passing.
Inheritance and subclassing are different. In inheritance, one imposes a constraint declaratively (say, “these objects must be a subclass of other objects”) and that can be done, often without any verification what so ever. Subclassing, in contrast, just exists even if one would not explicitly implement it. Consider:
The expected object was Y, now we substitute for some object X. This substitution only makes sense when X is compatible with Y.
There exists a compatibility relation between Xs and Ys, let’s call it the “compatible” relation.
If X is compatible with Y, and Y is compatible with Z, then X is compatible with Z. Every X is compatible with itself. There exists the most compatible object (say, nil, that can always be substituted). There exists the least compatible object (say, the empty object, which is compatible only with itself).
Just from substitution, we arrive at subclassing: our “compatible” relation now takes place of subclassing. This does not have to be checked by a compiler, it could equally persist only in the programmers’ mind.
Consider how subclassing works differently for: languages with inheritance declarations, algebraically typed languages (cf. coercions), un(i)typed languages.
One can also argue that the notion of “compatibility” only makes sense whenever one works with errors. Again, errors can be kept implicit or explicitly declared as exceptions. Without errors, every object could be substituted for another, and everything is compatible!
Why do I call them classes of objects and not just sets of objects? Technical, mathematical terminology: objects are non-well-founded, non-hereditary, graph-like constructions, while most people assume set theory to be well-founded, hereditary, tree-like.
Suggesting that Haskell has no null is doubtful. A diverging computation, e.g. null = 1 + null
is typable for, say Integers, but admits no value. So, there you go: another bottom value that fits in every type.
The nice thing about bottom, compared to null, is that it’s not observable. In other words, we can’t do something like:
myValue = if isBottom myOtherValue
then thingA
else thingB
In this sense, bottom acts more like a thrown exception (control flow) than a null (data value); although it looks like a null since laziness combines data flow with control flow.
In a sense, this more faithfully represents an “unknown” value, since attempting to figure out which value it is also ends up “unknown”. In contrast, null values are distinct from other values. For example, if I don’t know the value of a particular int
, the answer to “is it 42?” should be “I don’t know”, not “no”. Three value logic attempts to act like this, but is opt-in.
Just the idea that evaluation proceeds based on the definition of data, rather than separate control mechanisms, e.g. we can write ifThenElse
as a normal function:
ifThenElse True x y = x
ifThenElse False x y = y
Oh, I see. Thanks. I was thinking that the usual C-style control mechanisms, e.g. if
and for
, still kind of entangle control flow and data flow, albeit with special syntax rather than just functions. I wonder if it is possible to disentangle this? What would that look like?
A PBX such as Asterisk might be fun. Connct it to a (handheld) SIP; perhaps use a VoiceXML interpreter, and you can implement custom voice-based applications.
A very general theory for understanding computation is Rewrite Systems. A rewrite system can be understood as pattern matching on terms in some first-order language, binding free variables, and literally rewriting the terms into other terms. For example:
f(x,y) -> h(g(x),g(y))
Defines a rewrite relation, where x and y are free variables. Now an interesting general question pops up: given an arbitrary rewrite relation, and an arbitrary term, will you eventually reach a term for which no longer any of the patterns match? This is a reachability problem (and undecidable in general).
Other aspects of rewrite systems are: if you apply on any term two different rules, is it possible to join them back into a common term? This property is confluence and is also a general property of graphs. Joinability and meetability, and in particular partial order relations, are also understood intuitively as properties of graphs.
Benjamin C. Pierce, Types and Programming Languages, MIT Press.
That’s the one you want. I’m biased towards ML (vs Haskell), and I think the book is, too (it’s not a Haskell book). You can get all six, sure, but if you had to get one that’s the one.
+1 for this. I’m using TaPL in my PL class this quarter and it’s awesome. Super well written and ML is great for this class - the work involves writing successively more complex interpreters for successively more complex toy languages. We’re not sticking strictly to the book, but the sections our prof has pointed us to have been great.
I also highly recommend TAPL.
I’ve been recommended TAPL before, but seeing as this isnt a class thats strictly about type systems, I’d like to get a more general one and read TAPL later.
TAPL isn’t just about types neither - it’s types AND programming languages.
Practical Foundations for Programming Languages is also very good.
Lesson 1 of the Internet: read only. Lesson 2 of the Internet: everything on it is false, including this post.
Functional Programming and Object-Oriented Programming are dual, in a very precise way.
Data types and constructing inhabitant terms is dual to interface types and observation methods. Functions are interfaces with a single method that takes an argument and returns an argument. Isomorphic data types can be understood as existence of particular functions that map A to B and back from B to A, preserving identities. Dual to functions are so-called differences: these are data that witness an output argument belonging to an input argument. A basic argument could show that two classes are behaviorally equivalent whenever there is no difference between them (the differences between A and B, and the differences between B and A, are empty).
In Functional Programming, one is interested in the termination of a program. In Object-Oriented Programming, one is interested in the dual of termination: productivity of a process. Consider that the difficulty of preventing dead-locks is similar to the difficulty of ensuring termination.
In terms of logic, many advancements in recent years have brought us: constructive and computational interpretations of classical logics; languages that allow the expression of focussing on both the output of a program, and the input of a process; polarization of types to model within one system both functional aspects and objective aspects; better understanding of paradoxical mathematical foundations lead to the theory of non-wellfounded relations, which brings us the dual of recursion/induction called corecursion/coinduction.
In terms of abstract algebra, we now know that notions of quotient types of languages by certain equivalence/congruence relations is dual to notions of subtypes of abstract objects by certain bisimulations/bisimilarities of behaviors.
In terms of philosophy, it is understood that rationality and irrationality can also be applied to software systems. “The network is unpredictable,” is just another way of saying that the computer system consists of an a priori irrational component. Elementary problems in Computing Science, such as the Halting Problem, witness the theoretical existence of irrational components. Those who assume every system is completely rational, or can always be considered rational, suffer from a “closed world syndrome.”
From a layman’s perspective, I thnk it is dual in another way too. In terms of how mutability is handled. Functional way of organizing programs often strives to push the state out, with a set of pure functions inside, which are stitched together on some skeleton that handles state or IO. On the other hand, OO programming encapsulates the state, striving to provide as simple interface to the outside world as possible. i.e the mutability is hidden inside rather than pushed out.
Recently, I heard that quotient types are dual to subclassing. What do you mean with “non-termination of infinitary rewrite systems”? And, strategy is just a way to deal with non-confluence. Monads are the continuation-passing style translation that (formulas-as-types) corresponds to Gödels double negation translation of classical logics into constructivist logics, that is, embedding the computational interpretation of Turing machines into models of simulating interaction machines.
Empirical Software Engineering: I followed a course at my university on this. It was an eye opener. I can publish some of my reviews and summaries sometime. Let me already give you some basic ideas:
Finally, I became convinced that for most organizations software development is a huge liability. But, as a famous theoretical computer scientist said back in the days: we have to overcome this huge barrier, because without software some things are simply impossible to do. So keep making the trade off: how much are you willing to lose, with the slight chance of high rewards?
I’m also interested in that but online articles instead of books. The very nature of empiricism is to keep looking for more resources or angles as new work might catch what others miss. Might as well apply it to itself in terms of what methods/practices to use for empirical investigation. Let get meta with it. :)
If documents and models are unstructured, then consider using an unstructured model. An untyped language is actually typed with a single all-encompassing type. This can be simulated in any sufficiently powerful type system.
Consider, for example, Gson: it allows conversion into POJOs, thereby making use of existing data structures. But it is also possible to use Gson’s built-in all-encompassing type, and explore and navigate the unstructured JSON directly.
I don’t see any problem.
You can also add a variant class to make typed code somewhat typeless, ie. at my work we have a C++ wrapper around jsonc that puts everything into a tree with a variant class for the values that represents a bool, int, float or string. You can create a variant that represents as many values as you want to supports, with run time type safety. You can also assert or debug if the wrong type coercion is attempted.
To me, it seems like the type system equivalent of the safe vs unsafe debate in languages. The best practice on the safe side is to make it safe-by-default with an unsafe keyword that gives the developer freedom very selectively (eg per module). It becomes a big warning sign that the component needs strong code/data verification and validation. In this case, the dynamic typing could be the unsafe type of an otherwise statically-typed language that the program is implemented in. Just those things changing are marked with this unconstrained type with anything touching those variables validating the data they contain. Maybe some extra logging, too.
I also applied this tactic on one of my first jobs. At my desk, an A3 paper was beneath my keyboard, and I rested my arms on the thick paper. Everytime someone asked me to do something, or something popped in my mind, I wrote it on the paper.
Eventually, there were so many tasks on the paper that I applied some backpressure. I discussed the relevant tasks, to decide what was still necessary, and crossed out all other tasks. Tasks that were completed were marked by a checkmark.
After a few months, I got a little archive of A3 papers. This really helped me get a sense of progress.