Formal Methods of Software Design an Online Course by Eric Hehner | Hacker News Reader

Formal Methods of Software Design an Online Course by Eric Hehner

cs.utoronto.ca

I may be notorious, but not for the work I've done, rather for the misinformation about me that is repeated by people who don't check. I have written and published papers that say halting for programs in one formal system (language) cannot be solved in that same system, but can be solved in a different formal system. I would be delighted if you find an error in that work, but no-one has done so yet. I have never said that Goedel was wrong; I have written a paper explaining Goedel's results that other authors have used in textbooks and translations. I have never said Cantor's proof is wrong, but I have suggested there are other measures of set size than the one he proposed.

Mathematical results should never be accepted or rejected by whether you "trust this guy". You should read the work, think about it, and decide for yourself whether the results are right or wrong.

That's true, but trust is the way most everything is built outside of academics.

Why do we use X framework? Well, because Mr. Deep Pockets over there is using it!

I wish we could have a more mathematical world, but it doesn't scale beyond a handful of architects and really talented engineers.

The amount of hassle and push back I get for getting 100% code coverage tells me that it's rare for people to leverage more concrete and deeper ideas to even validate their thinking. The market rewards "just ship it" way more because ultimately customers just learn to manage the shit that ships.

Please correct me if I'm mistaken, but I did check a couple of years ago and found what I thought were some errors. I began to draft an email to you but never finished and eventually discarded it. I'll try to recreate it here:

With regards to halting, there are some programs that can be written simply in any common programming language to halt iff a solution to a specified number exists, simply by enumerating all possible values and halting if one satisfies the neccessary conditions. Thus to determine the halting of such a program would solve a problem. Typically these can be done in less than ten lines of Python, for instance. Some examples include: does there exist an odd perfect number; do there exist four positive integers a,b,c,n with n>2 such that a^n+b^n=c^n? The former is an open question; and the latter is Fermat's Last Theorem, which took an immense amount of machinery to prove, six decades after Turing's paper, and which is related to many open problems. (I've also heard that the halting problem could be used to solve the Riemann Hypothesis, but I don't know whether or not that's true.) If you can find a way to figure out whether or not such simple programs halt or not, I'd love to hear about it! What I've gleaned from your papers doesn't actually seem to apply to such programs though, which is a shame since these programs aren't very complicated.

Now, with regards to Cantor, I recall reading a paper on your website (which I can't seem to find today, so apologies if I misrepresent it). I agree that set theory is not a good way to evaluate the number of numbers, since it throws out all properties about such numbers (e.g. ordering); this is why we have natural density, real density, and other properties. But there was another part where you indicated (something to the effect of) that the reals were countable since there are countably many Turing Machines; however I believe the correct conclusion to draw is that there are uncomputable numbers. Again, I can't seem to find it today, so I apologize if this is unsubstantiated.

You point out quite correctly that if halting can be solved, then we can use it to settle certain open mathematical questions. But this does not tell us whether halting can be solved. (And if it can, it may not be a practical way to settle those questions.) I have many papers on the halting problem on my website at www.cs.utoronto.ca/~hehner/halting.html. The most recent is www.cs.utoronto.ca/~hehner/EGT+.pdf published in SN Computer Science v.1 p.308, 2020 September. Its final paragraph says: Let X and Y be two programming languages, or two computers, or two locations. It is inconsistent to ask for an X-program to compute halting for all X-programs due to a twisted self-reference. Twisted self-reference is characteristic of subjective specifications. So it may be consistent and satisfiable to ask for a Y-program to compute halting for all X-programs. At least it has not yet been proven impossible. If you want to know what a twisted self-reference is, or what a subjective specification is, you have to read the paper. This conclusion is not what you claimed it is. The Cantor paper you are unable to find is on my website. Its name is "the Size of a Set", and it is at www.cs.utoronto.ca/~hehner/SetSize.pdf. Its conclusion says: It is popularly believed that Cantor's diagonal argument proves that there are more reals than integers. In fact, it proves only that there is no onto function from the integers to the reals; by itself it says nothing about the sizes of sets. Set size measurement and comparison, like all mathematics, should be chosen to fit the needs of an application domain. For all application domains that I know of, Cantor's countability relation is not the most useful way to compare set sizes. I have never claimed, as you said, that there's anything wrong with Cantor's diagonal argument. My paper on Goedel, published in Beauty is our Business, Springer-Verlag silver series, New York, p.163-172, 1990, is at www.cs.utoronto.ca/~hehner/God.pdf. Nowhere in that paper is there any suggestion that "Goedel was wrong", as you claimed I said.

> So it may be consistent and satisfiable to ask for a Y-program to compute halting for all X-programs. At least it has not yet been proven impossible.

Alas, it has been proven. RAM computers are equivalent to Turing machines. If X and Y are Turing-complete languages then all X-programs can be converted to Turing machines, your proposed Y-program can also be converted into a Turing machine. Put another way, unless your language X is too weak to be useful, there should exist a deterministic program to convert any program written in Y into a program written in X with identical behavior (with regard to halting).

This should be evident by the fact that the computers we use day-in and day-out execute one binary machine language. Any X-program and Y-program reduce to the same assembly language.

The twisted self-reference must therefore be language-agnostic. You can absolutely solve halting for various simplified "languages", but not Turing-complete languages.

Here's a sketch of a proof explaining why this is impossible (under the Church-Turing thesis).

Suppose you have written a Y-program y that takes an X-program x as input, and computes whether or not x halts (say, on no input), AND y halts every time.

If X is a Turing-complete language, then for a given Turing Machine t we write an X-program xt that simulates t and halts iff t does. Then we run y on xt. This decides whether or not t halts, and works for all TMs t; therefore y solves the halting problem for all Turing Machines. But we know from Turing's "twisted self-reference" that no Turing Machine can do this, so the language Y must be strictly more computationally powerful than the Turing Machine model. This would disprove the Church-Turing thesis, which would be pretty incredible if true, but seems highly unlikely (since modern computers, and even quantum computers, are polynomial time equivalent to TMs).

Otherwise, X is not a Turing-complete language. This is valid, I guess, but not really relevant to the problem of halting, since such a language would be very underpowered for most useful purposes. Now, regular languages are decidable, which is great for lots of computations that can be encoded using predicate logic and first-order arithmetic. Even climbing one rung up the computational complexity to context-free languages brings undecidability, though, since many problems (e.g. whether or not two context-free grammars generate the same language) are undecidable.

Regarding Goedel, I apologize and retract my claim.

Regarding Cantor, indeed, there are many ways to compare the "sizes" of two sets. Cardinality is one such way. It can have applications, for instance Cantor's original paper used it to prove that there are infinitely many transcendental numbers. It is also used in real analysis, in Lebesgue integration, and in measure theory. But it is not the only way to do so. There is a very real sense in which {1,2,3} is a smaller set than {4,5}; that does depend on knowledge of the contents of the set though, not merely the number of elements contained. In a more abstract context where measure or natural density aren't applicable, cardinality can be left as the only well-defined definition of "size", but in most contexts I agree, it's just one of many possible definitions and they should each be used with care.

Arguing about the sizes of different infinite sets is tricky, though. The set of even integers has the same cardinality as the set of all integers, even though it has density 0.5. The cardinality of the set of rationals is somehow "infinitely less" than the set of irrationals, even though both sets are dense on one another. But there are some things we can learn from not having

Me, however, I like cardinality for the aesthetic properties. I like the Axiom of Choice and all the nonsense that follows from it. Cardinal infinities behave quite differently from the well-defined infinities of ordinals, hyperreal numbers, and surreal numbers.

In your article "The Size of a Set", you discuss Formalism. Are you aware of the axiom "V=L"? It's quite neat, because by effectively outlawing any non-constructible sets, the Generalized Continuum Hypothesis follows! If you accept cardinality as a purely aesthetic definition in conjunction with Formalist ideology, you get a very beautiful result. Practical, maybe not, but beautiful.

That is all to say that I agree with a lot of what's in your paper on "the Size of a Set". However, the "Program Analogy" section of the paper contains what I think is a flawed argument:

> [A] Cantor-type conclusion concerning the sizes of sets of programs is absurd. The proper conclusion is simply that there is no program (in some programming language) to generate all and only the infinite-sequence programs (in that same programming language). It is not a conclusion about the sizes of sets. Likewise in the original Cantor argument, the proper conclusion is not about the sizes of sets; it is simply that there is no sequence of all infinite sequences.

I think the correct conclusion here is that to determine which programs are "infinite-sequence" is undecidable. You've reached a contradiction, therefore the last assumption must be flawed; in this case the assumption was that you could write a program D "whose execution neither halts nor goes into a non-printing infinite loop." This assumption is about programs and programming languages, and says nothing about sets, so the analogy is flawed. In Cantor's argument, the assumption is that the set [0,1) can be ordered. You're correct in saying that this is merely a statement about the existence of a bijection between the naturals and the reals, but that is the definition of cardinality. Your issue here is that you don't like saying that cardinality means "size", and that's fair. But I think this analogy is a stretch at best, and irrelevant to your overall argument.

I said: So it may be consistent and satisfiable to ask for a Y-program to compute halting for all X-programs. At least it has not yet been proven impossible.

You said: Alas, it has been proven. RAM computers are equivalent to Turing machines. If X and Y are Turing-complete languages then all X-programs can be converted to Turing machines, your proposed Y-program can also be converted into a Turing machine. Put another way, unless your language X is too weak to be useful, there should exist a deterministic program to convert any program written in Y into a program written in X with identical behavior (with regard to halting). This should be evident by the fact that the computers we use day-in and day-out execute one binary machine language. Any X-program and Y-program reduce to the same assembly language.

I say: You cannot have read my papers carefully. I spent a lot of time explaining, with examples, why programs with subjective specifications cannot be translated from one TM-equivalent language to another TM-equivalent language.

You said: This would disprove the Church-Turing thesis.

I say: Again, you cannot have read the paper carefully. There is a section in each of www.cs.utoronto.ca/~hehner/OSS.pdf and www.cs.utoronto.ca/~hehner/EGT+.pdf titled "Church-Turing Thesis", explaining that it applies to all objective specifications, which are the only specifications considered by Church and Turing, but not to subjective specifications.

You said: Regarding Cantor, indeed, there are many ways to compare the "sizes" of two sets. Cardinality is one such way. It can have applications, for instance Cantor's original paper used it to prove that there are infinitely many transcendental numbers. It is also used in real analysis, in Lebesgue integration, and in measure theory.

I say: Again, you cannot have read the paper carefully. Almost every time I mention applications in the paper, I say "applications outside mathematics". If you consider mathematics to be an application of mathematics, then all mathematics has applications.

You said: the "Program Analogy" section of the paper contains what I think is a flawed argument.

I say: Yes, I point out the flaw in the paper in the paragraph that starts with the sentence "Like the original Cantor argument, this program-analogy version is informal, and the informality may hide serious errors.". Did you miss it?

You will "win" this debate by throwing misunderstandings at me faster than I can reply. And it's disheartening because the replies are already in the papers, if you read them carefully.

> I say: You cannot have read my papers carefully. I spent a lot of time explaining, with examples, why programs with subjective specifications cannot be translated from one TM-equivalent language to another TM-equivalent language.

> I say: Again, you cannot have read the paper carefully. There is a section in each of www.cs.utoronto.ca/~hehner/OSS.pdf and www.cs.utoronto.ca/~hehner/EGT+.pdf titled "Church-Turing Thesis", explaining that it applies to all objective specifications, which are the only specifications considered by Church and Turing, but not to subjective specifications.

Fair point, I had not read OSS. That said, I think your interest in "subjective specifications" goes against your apparent disinterest in the "twisted self-reference" of Halting Problem proofs. It throws readers off as you attempt to add twisted self-reference to the domain of programming, where it isn't usually found, and simultaneously remove it from other places where it emerges naturally (as a consequence of the Church-Turing Thesis).

> I say: Again, you cannot have read the paper carefully. Almost every time I mention applications in the paper, I say "applications outside mathematics". If you consider mathematics to be an application of mathematics, then all mathematics has applications.

Fair point, I concede.

> I say: Yes, I point out the flaw in the paper in the paragraph that starts with the sentence "Like the original Cantor argument, this program-analogy version is informal, and the informality may hide serious errors.". Did you miss it?

No, I didn't miss it, but the inclusion of such an irrelevant and flawed analogy is perplexing and makes the paper harder to read, and seem less worth the time it takes to read carefully. You've written a lot, and some of the material can be tough to chew through (especially that written with the structure of formal logic).

> And it's disheartening because the replies are already in the papers, if you read them carefully.

https://www.youtube.com/watch?v=HMqZ2PPOLik

I've reread your OSS and EGT papers, with the additional help of your comments above, I think I now understand your stance better. I think part of your notoriety comes from your papers appearing to contradict the Halting Problem, with sections titled "How to Solve Halting" that don't actually provide a clear method. Instead, emphasizing that you're examining self-referential logic puzzles reminiscent of those found in Raymond Smullyan books would help clarify what you're doing. Many readers come in with the Bernard Russell mindset of "Let's try to avoid these self-referential questions" and thus have trouble adjusting to your angle. Most readers interested in The Halting Problem are not interested in "subjective specifications."

Your papers aren't easy reads (and I'm not complaining: it's an unavoidable consequence of their nature as papers on self-referential logic) and a brief first pass of your papers leaves many of us misinterpreting your angle. I think some editing of your introductions and conclusions could help immensely. Be very upfront and explicit that you don't disagree with the common conclusions of The Halting Problem for objective specifications, but instead that you're more interested in exploring a different side of programming. (In this regard, Jeffrey Shallit's mean-spirited "fringe computer science" comments make sense, but really ought not to be an insult since you are in fact exploring an oft-ignored side of the field.) Err on the side of caution, and over-communicate your intent with the papers! When many readers think you've said X when you have not, in fact, said X, take that as constructive feedback to more explicitly say "not X" in edits and future papers.

Thank you for guiding me in reading your papers. Your arguments in this thread have helped me make sense of them. I think I finally understand your arguments, and I hope with a change to your approach, you can successfully reach other readers too.

Your advice is good.

Here is a YouTube playlist, for those who don't want to download the individual *.mov-files and are OK with streaming via YouTube.

https://www.youtube.com/watch?v=89fKiaMxHrA&list=PLfsVAYSMws...

I've done this course. It's interesting and makes you think, would recommend if that's what you're looking for.

While not my area of expertise, I don't this course is particularly relevant to any practical modern formal methods unless you want to reinvent the world.

I took both the intro and advanced version of this course in my undergrad. Academically interesting stuff, but the inability to translate from proved system to implemented and proved system was always frustrating.

It was definitey a clear delineation between _computer science_ and _engineering science_ during my undergraduate courses.

It it applicable to the "practical" (or practiced?) software development?

I wouldn't say so, maybe slightly in that it might help with thought patterns a bit, but in the way that studying advanced mathematics might help not as in you're likely to directly use the skills.

Thanks for putting it in context. This is exactly what I'm looking for. (making it practical, I'll take care of that myself).

Do you have any suggestions for courses teaching practical formal methods?

These aren’t courses, but I recommend looking at TLA+ and Alloy. Some of my colleagues use Isabelle, Coq, and Agda too, but the first two seem most relevant to learn.

I've also heard good things about lean.

I forgot about Lean, but yeah I’ve heard good things too! Hillel Wayne has a good email list I recommend where he sends weekly posts on different tools :)

This course inspired my research on teaching binary tree algorithms using visual programming:

https://ieeexplore.ieee.org/abstract/document/545265

http://opsis.sourceforge.net

I really like Eric's work, especially "From Boolean Algebra to Unified Algebra".

His algebraic approach towards building software is really refreshing as it starts with the absolute basics and then slowly builds to a whole framework. Recommended!

Dunno how much I trust this guy. He's notorious for claiming that the Halting Problem is actually solvable, and in other places suggests that Godel was wrong, and even that Cantor's proof that the reals are uncountable is wrong. http://www.cs.toronto.edu/~hehner/halting.html Finding the flaws in all those arguments is a good challenge if you have a free afternoon!

FYI, Eric has replied to your post, but on the root of the discussion.

He's somewhat of a crank, but the math in this course is approachable and correct, and the ideas interesting. It was also created... awhile ago.

One previous thread:

Formal Methods of Software Design: an online course by Eric Hehner - https://news.ycombinator.com/item?id=6464463 - Sept 2013 (8 comments)

I want to say stuff like this will never show up in your career, but then competition level algos started showing up in the interview.

Might be a chance to get ahead of the curve here, bookmarked. This looks interesting and challenging, but maybe not realistic. Prime candidate to grind out 1000s of these exercises.

The vast majority of developers will never encounter this stuff in the way it's being presented. Sometimes you'll be hacking together some version of a js framework to get some UI feature using the patterns permitted by company A in a very narrow scope. In a practical sense, that's not using the concepts as much as stumbling across them.

I guess you are making my point. If the zeitgeist picks up that formal modeling captures intelligence, then it will make its way into the hiring process just like competitive programming did via Leetcode.

I wonder if anyone has some thoughts on the application of methods like this in the realm of machine learning modelling? I'm very interested in the concept and can see there must be a link but haven't yet thought my way into it

There is a bit of research going on in the space between programming languages and machine learning. Mostly it is about probabilistic programming and Bayesian methods etc.

However, using type theory to assist in writing models is something I am currently looking into. It is an interesting area that has the potential to propel the development of seriously large models.

I've been working on something somewhat related. Would be happy to have a chat if you like.

Is there something like this with math? Linear Algebra specifically?

If you want to write software using principles from linear algebra you should definitely google some computer graphics courses

I laughed at formal methods of program proof until I came across a simplified version of cleanroom development methodology (which breaks program components into 'program primes' like A then B, If A then B, While A do B and for A in B do C) that allowed you to formally prove outcomes on paper. I have long since lost the document but to this day, I construct most of my work around these primes for certain projects.

That sounds a bit like Hoare logic [0], refinement calculus [1], or guarded command language [2]. The term "program prime" is not something I've heard or read before and I'm not turning up much.

[0] https://en.wikipedia.org/wiki/Hoare_logic

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

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

I found mention of "program primes" and "cleanroom" in the index of this book [0], but they are rather far apart from one another.

[0] https://svkarthikwinner.files.wordpress.com/2015/07/practica...

Goodness knows why my original comment is being downvoted. The formal term is 'primary program refinement' and can be found all over the place such as here:

http://p.web.umkc.edu/pgd5ab/cs_451/HW3/hw3.htm

Reply on news.ycombinator.com