Mathematics for Computer Science (2024)
ocw.mit.edu
ocw.mit.edu
Although I have always been struggling with keeping up with long lecture playlists. I always try to find shorter videos which explain the concept faster (although probably lacking depth). And end up ditching it halfway as well. Perhaps the real motivation to keep up with the material comes from actually enrolling the university? Has anyone completed such type of lectures by themselves? How do you stay consistent and disciplined?
I find courses in some platforms (coursera/khanacademy) a bit more motivating because they kind of push me with deadlines. I guess I am used to deadline-oriented studying.
If anyone else is struggling with attention span and is looking for shorter lectures (although they may not have the same depth): https://www.youtube.com/@ProfessorDaveExplains/playlists
I think long lecture playlist is a feature, not a bug. It's much harder to commit to such material when you're not full timing education.
Major weaknesses are some cool sections like Linear Algebra that have no exercises in their respective "tree", but that's very rare.
A bit of a side note but I find that the lectures are not the most interesting/useful part of those courses. The problem sets and the time spent trying to solve them ended up solidifying so many ideas that I had fooled myself into believing I understood. So I highly recommend heads-down solving some problems. It sinks much more time than the lectures but you come out of it better off
Without a very experienced mentor, I think it's very difficult to get to the independent-learning stage with math. That's the key. You need someone to go through your work, correct you, and make sure you don't go off in a very wrong direction.
So my advice is find at least a graduate student in math to help you. It's like a piano teacher, if you've ever taken piano, you know it's absolutely mandatory to have a teacher. People who self-learn from the start end up being able to play but not very well.
Edit: one other crucial component is time. If you're really interested in knowing something like linear algebra, analysis, or calculus with fluency, expect to spend at least 10 hours per week on it for a year. Two hours per week will give you a cursory and very weak understanding only.
Self taught people often skip too much of the basics so they struggle to properly tackle the fancy stuff
They only see the superficial or easy-to-spot goals and lack the eye for detail to build foundations and technique.
You need to guide your own study and you might not know what you need to learn to get unstuck
Many teachers cannot do that either.
I find ChatGPT and the Gemini model quite good at problems whose solutions are already known. We just need the Wille—the will—to ask it.
Of course there are bad teachers out there. The question wasnt "are there human yeachers as bad as an LLM" it was whether an LLM is as good as a good human teacher
> We just need the Wille—the will—to ask it.
Thats the thing. Its is a very good search resource. But thats not what a teacher is. A good teacher will help you get to the right questions, not just get you the right answers. And the student often wont know the right questions until they already know quite a bit. You need a sufficiently advanced, if incomplete, mental model of the sybject to know what you dont know. An LLM cant really model what your thinking, what your stuck on, and what questions you should be asking
I believe that through a few common prompts and careful reflection on the LLM's responses, this challenge can be easily overcome. Also, nobody truly knows what you're stuck on or thinking, unless you figure out the existence of unknown and seek it out. However, I do agree with your point that "a good teacher will help you get to the right questions," since a great teacher is an active agent; they can present the unknown parts first, actively forcing you to think about them.
- when people see some things as beautiful(best), other things become ugly(ordinary)....Being and non-being create each other. — Laozi, Tao Te Ching
Perhaps the emphasis on the greatness of an LLM gives the impression that it undermines the greatness of a great human teacher, which has already led to a few downvotes. I want to clarify that I never intended to undermine that. I have encountered a few great teachers in my life, whether during my school years or those teaching in the form of MOOCs. A great teacher excels at activating the students' wille to seek the unknown and teaching more than just knowledge. Also, the LLM relies heavily on these very people to create the useful materials it trains on.
Metaphorically speaking, the LLM is learning from almost all great teachers to become a great 'teacher' itself. In that sense, I find no problem saying "LLM could be the teacher, one of the best already."
The best use of an LLM I've found in learning is for when I explain to it my understanding of what I learned and have it critique what I've said. This has greatly reduced the amount of backtracking I need to do as I start to realize I've misunderstand a foundational concept later on when things stop making sense. Often simply having the model response with "Not quite, ..." is enough to make me realize I need to go back and re-read a section.
The other absolute godsend is just being able to take a picture of an equation in a book and ask for some help understanding it notationally. This is especially helpful when going between fields that use different notation (e.g. statistics -> physics)
This was exactly my situation. Videos can give you a lot of structured, well presented information. And for MIT courses you'd get this knowledge from the very best. The problem is that no matter how well the subject matter is presented, I would hit some conceptual snag that I couldn't resolve just by repeating the sections in the video.
Now, years ago, to clear up the concepts, I would go to math stack exchange, write down exactly what I wanted to understand using mathjax and hope that someone will provide a detailed enough explanation. Most of the time I did learn from the answers, but sometimes the answer would be too succinct. In such cases there would be a need for a back and forth and stackexchange is not really designed around that usage pattern. This hassle would eventually make me give up the whole endeavor.
Now however there are LLMs. They don't need mathjax to understand what I am talking about and they are pretty good at back and forth. In the past 6 months I have gone through 2 full MIT courses with practice sheets and exams.
So I would encourage anyone who went through the route of self learning via videos and found it to be too cumbersome and lacking to give it another go with your favorite LLM.
What the LLM still does not provide is accountability (a LLM isn’t going to stop you from skipping a problem set) and the human social component. But you could potentially get that from a community of other self-learners covering the same material if you’re able to pull one together.
Too many times I've used LLMs for tasks at work and some of the answers I've gotten back are subtlety wrong. I can skip past those suggestions because the subject is one I'm strong/experienced in and I can easily tell that the LLM is just wrong or speaking nonsense.
But if I didn't have that level of experience, I don't think I would be able to tell where the LLM was wrong/mistaken.
I think LLMs are great for learning new things, but I also think you have to be skeptical of everything it says and need to double check the logic of what it's telling you.
But it might still help, especially if you think about the LLM as a fellow student rather than as a teacher. You try to catch it out, spot where it's misunderstood. Explain to it what you understand and see if it corrects you?
I am amazed at those wo fought or even flourished through that.
Then again, William & Mary had some incredible teachers, and maybe the online program through a different school just isn’t very good at designing assignments and teaching by comparison. But I feel that there was a difference in how I could succeed at challenging assignments when I was among other students in a social setting. The work in undergrad was highly rigorous, though exploring it alongside other real-life students made it a very different undertaking.
Not sure why you added "but even so", getting a PhD is fundamentally about believing in the necessity of the mentor/mentee relationship for learning. It's not at all surprising that you would find:
> You need someone to go through your work, correct you, and make sure you don't go off in a very wrong direction.
I've learned enough to publish (well received) technical books in areas I've never taken a single course in, and have personally found that in-classroom experiences were never as valuable as I had hoped they would be. Of course starting from absolute 0 is challenging, but one good teacher early on can be enough.
Though I also don't think video lectures alone are adequate. Rather than focusing on "exercises", I've found I get the biggest boost in learning when I need to build something or solve a real problems with the mathematical tools I'm studying. Learning a bit, using it to build a real project, and then coming back when you need to unblock the next hurdle is very effective.
On top of this, books are just better for learning than videos (or lectures in general). Lectures are only useful for getting the lay of the land, and getting a feel for how types of problems are worked out. Especially with mathematics, you need time to look at an equation, read ahead, flip back, write it in a notebook, etc until you really start to get it.You really can't possibly get any of these ideas in 45-60 minutes of someone talking about it.
That's why, for me, online lectures don't really change the autodidact game all that much. Reading books and solving problems seems to have been the standard way to learn things well for at least the last several hundred years, and lectures don't improve on that too much.
Because the "even so" was for the "self-motivated" part, not the "getting the PhD" part.
> I've learned enough to publish (well received) technical books in areas I've never taken a single course in,
I'm talking about pure math here, not other technical fields which are more hands on and don't require as much mentorship. Programming is easier to self-learn than math for sure, because it is not very abstract compared to math. It's also guided by whether the code works or not.
Well the post is "Mathematics for Computer Science" which I don't think anyone considers "pure math". Most of my writing has been in the area of applied mathematics, the closest I've gotten to pure math would be some stuff on measure theory.
So yea, it might be a challenge to self teach something like cluster algebras, but at that level much of the work in the field is academic communication anyway.
I would recommend pairing it with:
https://ocw.mit.edu/courses/6-001-structure-and-interpretati...
and some additional online resources which I've found very helpful:
- https://mathcs.clarku.edu/~djoyce/java/elements/elements.htm...
- https://www.motionmountain.net/
and of course https://librivox.org/ and https://www.gutenberg.org/ --- for a benchmark on why, well, when my father retired to a rural Virginia county, the library was a metal carrel of books in the basement of the old courthouse, and my favourite books during the summer (when I didn't have access to the school libraries) were Hal Clement's _Space Lash_ (which my father found in a tower at the prison where he worked where reading material was forbidden) and an English textbook containing a number of short stories which my mother purchased from a table of remaindered books in a department store in a town 26 miles away to which we might drive once a month or so.
Also, be modest and assume you're dumber than you think you are - start with courses where you already know at least 50% of materials covered.
I’m thinking about enrolling in an online college just for fun. Though the problem I have is that I think the Venn diagram of colleges that are online, aren’t expensive, have advanced CS/ML courses, have an experienced professor that you get to interact with is pretty much zero. If anyone has suggestions, do let me know.
You have a finite amount of energy in a day and learning takes a lot of energy. It's why a kid's job is the learn.
You could try front running the learning, but it will impact your energy levels at work. It still takes a monumental amounts of discipline, but you may have the energy to make it work.
This is about weight loss, but I think it can be applied to anything:
https://www.medicspot.co.uk/weight-loss/behaviour-change/pub...
For most people in most situations, the real motivation to keep up with the material comes from the wage premium one gets after getting the sheepskin. It is unsurprising you, a humble autodidact, are having a lot more trouble than an actual MIT student, because unlike an actual MIT student, you will not walk out of this course any closer to having an MIT degree.
>I guess I am used to deadline-oriented studying.
You can always reverse the curse, and promise to pay someone if you don't finish X material by Y date. You probably also want some kind of proof mechanism to show that you actually did it, like eg a graded test.
>Has anyone completed such type of lectures by themselves? How do you stay consistent and disciplined?
I've read through several textbooks cover to cover including problem sets since graduating. My motivation is mostly just burning curiosity. I can't stand the feeling of not only not knowing a thing, but knowing that I don't know it or feeling like I'm faking it every time I do act on what I know.
But it is completely true. No one would ‘learn’ the way college courses are structured. The only reason these courses get completed is the pace/cadence, GPA requirements to get jobs and the degree.
In the ‘real world’ you just learn enough to solve the problem in front of you and as you face more and more your knowledge tree expands.
No one in their right mind would go through a syllabus-like sequence - it is just boring, dull as hell.
It's only cynical if you think making money is bad! I think it's terrific that your average B student and up is mature enough to reliably take on tens of thousands of dollars in debt, and work hard for several years without any immediate reward, in exchange for a pretty reliable pathway towards high paying specialized labor for the rest of their lives. It spits in the face of the narrative that young people are too stupid, or too naive or whatever to have agency in their own lives.
>The only reason these courses get completed is the pace/cadence, GPA requirements to get jobs and the degree.
I cite The Case Against Education, as usual. [1]
>In the ‘real world’ you just learn enough to solve the problem in front of you and as you face more and more your knowledge tree expands. No one in their right mind would go through a syllabus-like sequence - it is just boring, dull as hell.
I cite too John D. Cook's "Just-in-case versus just-in-time" blog post. [2] I don't work through actual syllabi, but I love working through textbooks from start to finish. But you are also correct that I am emphatically not in my right mind, and my career has suffered for it. ;)
[1]: https://www.youtube.com/watch?v=_t957pTcJ0E&t=2s
[2]: https://www.johndcook.com/blog/2010/03/03/just-in-case-versu...
Even if it is true that in the moment you aren’t focused or whatever other excuses your mind comes up with, so what? “Go to class” anyway. At worst you learn nothing but improve your discipline skills.
Set a regular time to watch the lectures so you can’t lie to yourself about doing it later.
I want to be clear, it isn’t about willing yourself through it despite everything even if it can read that way. It’s about honoring the choice you made to attend to the lectures and not accepting excuses from your mind.
Recognizing that you can choose, recognizing that past you had good intentions for you and deserves you to honor those intentions, and recognizing that your thoughts and feelings in the moment may not be true and “aren’t the boss of you” even if they are true helps tremendously.
So many cool (free) courses and so easy to find, download.
But also remember, many of those lectures are at a slower peace, so one or two lectures per week. It takes time to internalize the material. People that don't follow university usually try to binge watch them, but this leads to low outcomes.
I think the best strategy is to put deadlines and risks for yourself, and follow them at a natural peace. And, do the exercices.
https://ocw.mit.edu/courses/6-1200j-mathematics-for-computer...
Lecture notes:
https://ocw.mit.edu/courses/6-1200j-mathematics-for-computer...
There are a few unusual parts, like the last lecture ("Large Deviations"). I'm not familiar with the entire course, but IMO the lecture on state machines is very good; it discusses invariants and uses an approchable example (the 15-puzzle).
Text (last revised 2018): https://courses.csail.mit.edu/6.042/spring18/mcs.pdf
If you have never looked at it, the problems there are very nice. For example, instead of some dry boolean logic problem about A and Not(B), you have Problem 3.17 on page 81, which begins:
This problem examines whether the following specifications are satisfiable:
1. If the file system is not locked, then. . .
(a) new messages will be queued.
(b) new messages will be sent to the messages buffer.
(c) the system is functioning normally, and conversely, if the system is
functioning normally, then the file system is not locked.
[...]
(a) Begin by translating the five specifications into propositional
formulas using the four propositional variables [...]They do give an example of a Chernoff (exponential) bound for a sum of iid random variables. The bound of course has an exponential form - they just don’t call it a large deviation. So it’s a bit of a missed opportunity, oven that the name is in the chapter title.
These bounds come up all over the place in CS, but especially lately in learning theory.
Not to knock it. I've been working through quantum computing between work-related fire drills and household commitments, so I should be up to speed in a few decades.
At that time, if you wanted to do application programming, you took software engineering (OO Pascal and C++) or computer technology (Java) from either tech or engineering schools.
Such courses are generally titled "Intro to".
https://www.linkedin.com/posts/lean-fro_leanlang-cslib-forma...
If you don't know, writing a proof in isolation can be difficult, since you may be writing on that isn't actually sound.
I just think this is a distraction unless your goal is to learn lean and not math.
Errors are found in human proofs all the time. And like everything else, going through the process of formalizing to a machine only increases the clarity and accuracy of what you’re doing.
Over-emphasis on formalism leads me to conclude you just don't understand the purpose of proofs. You are primarily interested in formal logic - not math.
I would invite you to read a few pages of famous papers - for example Perelman's paper on the Poincaré Conjecture.
Of course, these MIT lectures are aimed at computer scientists, not software engineers, which US universities consider to be quite different.
Not true. He/She doesn't need to know all of it nor in depth but a conceptual understanding is very much needed to write "correct" (w.r.t. a specification) code. We Humans are natural algorithmic problem solvers and hence can always muddle our way through to a ad-hoc solution for a given problem. Obviously, a lot depends on the intelligence of the individual here. What Mathematics gives you is a structure and concepts to systematize our thinking and rigorously apply it so that problem solving becomes more mechanical. Thus you learn to specify the problem rigorously using mathematical concepts and then use mathematical logic to derive a "Program" satisfying those requirements.
At the very least a knowledge of Set Theory, Logic and Relational Algebra goes a long way towards understanding the mapping from Mathematics to Computer Programming.
The following books are helpful here;
1) Introductory Logic and Sets for Computer Scientists by Nimal Nissanke. A very nice overview and wide coverage of needed basic mathematics.
2) Understanding Formal Methods by Jean-Francois Monin. A fire-hose overview of mathematical models and tools implementing those models.
I know all these from university, but I did programming and SQL before that without any issues. Learning these mathematical details seemed really not useful in practice, at least for me.
Of course, coming up with something like SQL in the first place requires a lot of theoretical mathematics (set theory, relational algebra), but as someone who only uses those systems, like 99% of software engineers, understanding the mathematical theory here doesn't seem very helpful.
As a first approximation; a) Type = Set b) Function = subset of Relation (i.e. set of Tuples) obtained from Cartesian Product of {input type set X output type set} c) Logical conditions define new relational sets where its members have a ordering relation d) A Program is a series of functions which prune and transform the tuples from the above cartesian product.
A Program then becomes a trajectory enforced using predicate logic through a state space obtained from the cartesian product of all the types in the program.
You are using all of the above whether you know it or not when programming in a high-level language. The real value comes when you do it with the knowledge of the mathematics in hand because then it allows you to prove your Program as "Correct" (w.r.t. a specification).
Exactly. The average programmer doesn't have to know the math behind things like types to use them.
> The real value comes when you do it with the knowledge of the mathematics in hand because then it allows you to prove your Program as "Correct" (w.r.t. a specification).
I don't think the average software engineer does that or would benefit from doing it. I certainly don't.
Again; you are drawing the wrong conclusions and projecting your own ignorance on others.
To give a simple analogy; anybody can swing a baseball bat at a ball. But that won't make him a notable player. To become a superlative player one needs to understand body dynamics and train scientifically. In a similar vein, anybody can muddle through and come up with a Program. But more often than not, it will be error-prone and bug-ridden not to mention hard to extend and maintain. Given the importance of Software to our modern society this is not what we want. A little bit of knowledge of Mathematics behind Programming gives you orders of magnitude return in software quality which is absolutely worthwhile.
There is nothing to debate/argue here but merely pointing out the application of scientific method to software engineering.
I reject your accusation. It's more likely that you are the one who is projecting, namely your ignorance of what the average software engineer is doing.
As mentioned earlier, the point of studying Mathematics for Computer Science is to make your "average software engineer" better and more productive than he/she was in the past.
Eugene Wigner's classic essay The Unreasonable Effectiveness of Mathematics in the Natural Sciences is very relevant here - https://en.wikipedia.org/wiki/The_Unreasonable_Effectiveness...
At the risk of nitpicking:
Certainly it's a benefit to structure and understand code such that you can reason about it effectively, but prove goes too far. Almost no real code is proven correct, the ergonomics of formal methods are still far too poor for that.
The point was that a knowledge of the requisite Mathematics gives you a very powerful way of viewing Programs and then you get to choose how to map/implement it using any number of tools and based on the needs of the software.
If you want to prove your program's correctness, that's the domain of formal methods, essentially by definition.
A Formal Method defined broadly is the application of Mathematical Concepts/Models and Logic to the specification/implementation/verification of Computer Programs.
DbC is based on Hoare Logic where you try to "prove" the program intellectually and not necessarily tool driven. This was somewhat mechanized (though still a intellectual pursuit) by Dijkstra's technique of deriving weakest-preconditions. Because the whole process can be quite tedious, laborious and rather complex, automatic theorem prover tools were invented to do the job for you. This has resulted in the unfortunate status quo where Formal Specification/Verification have become identified with the use of tools and not the Mathematics behind them. Proving Correctness need not be fine-grained and absolute but can be good enough done partially at a gross level at specific stages in a program as needed and done either by hand and/or using tools.
DbC can be considered a lightweight Formal Method with aspects of both Specification and Verification included. The Programmer plays the role of "theorem prover" when using DbC. However tools exist to map "Design-by-Contract" constructs to "Verified Design-by-Contract" constructs. See for example https://www.eschertech.com/products/verified_dbc.php. Also Eiffel (quintessential DbC language) can be converted using AutoProof to a form which can be proven by Boogie verifier.
Finally; here is a case study Design by contract formal verification for automotive embedded software robustness (abstract & pdf) - https://hal.sorbonne-universite.fr/ERTS2024/hal-05028176v1
I feel I need to insist on this point: a design-by-contract methodology using runtime checking may be an effective means of improving software quality, but it certainly isn't proving the correctness of a program. Using the word 'prove' here is just plain wrong. Putting it in quotation marks doesn't help. It simply does not constitute a proof.
> It is a very narrow and wrong way of looking at Formal Methods (both Specification and Verification) and one of the main reasons the "ordinary" software engineer gets intimidated and overawed by formal methods and afraid to even approach the subject
I'm not insisting on a narrow understanding of formal methods, I'm insisting on proper use of established terminology.
I'm all for practical methodologies that benefit software quality without paying the enormous costs of fully applying formal methods. Design-by-contract with runtime checking seems like a reasonable approach. (Static typing is another. Effect-oriented programming might be another.) My point was just about the proper use of the word proof.
> Proving Correctness need not be fine-grained and absolute but can be good enough done partially at a gross level at specific stages in a program as needed and done either by hand and/or using tools.
A program is proven correct only when the proof is absolute, which implies fine-grained. I'm not opposed to the use of partial proofs or 'good enough' proof-sketches, both of which could be useful in producing high-quality software in the real world, but we should be clear in how we refer to them.
I'm not sure about the idea of proving correctness by hand, though. Manually applying a formal model of a real programming language sounds unworkable. If code is well structured, it should be possible for the programmer to reason about it somewhat precisely, like a proof-sketch, but that's not a proof of correctness.
> The Programmer plays the role of "theorem prover" when using DbC
I don't find this convincing. There's nothing stopping the programmer from failing to notice some error. If you aren't actually doing a proof, just say so. There is no stand-in.
> tools exist to map "Design-by-Contract" constructs to "Verified Design-by-Contract" constructs.
Right, I hinted at this in my previous comment. SPARK Ada does this. In that case, correctness properties of the program are indeed formally proven. That's a quite different methodology to design-by-contract with runtime checking though, to the point that it almost seems unhelpful to refer to them both by the same name. I've had to be careful to explicitly state design-by-contract using runtime checking this whole time.
The deeper distinction here is between testing and formal proof, and design-by-contract can in principle refer to either.
> here is a case study Design by contract formal verification for automotive embedded software robustness
Have only skim-read but seems somewhat similar to this case-study about SPARK: https://www.adacore.com/tokeneer
The reason is because Mathematics deals with ideal and abstract objects whereas objects in the real world (eg. a computer program) can only map to aspects of the ideal world and not in its entirety.
To elaborate; a mathematical algebraic system is a set of objects and a set of operations defined on them. Axioms using those objects/operations are then defined and then inference/reasoning rules using these are defined to prove theorems in the system. There are various techniques for constructing proofs (eg. direct, induction, contradiction etc.) but all of them must map back to the domain of definition of the objects in the algebra to be considered valid and sound in the real world.
As an example, the axiom of associativity w.r.t. addition holds absolutely in mathematics when applied to {N, +} where N is the infinite set of ideal integers. But in computing it is not always the case i.e. (a+b)+c =/= a+(b+c) always because a/b/c are constrained/partial finite sets (i.e. int8/int16/int32 etc.) and thus the axiom of associativity will fail when for example, we take boundary values for a/b and a negative value for c (due to overflow/underflow). Thus any proof which uses the axiom of associativity for signed integers in a computer can never be as absolute and general as its counterpart in pure mathematics i.e. everything is Partial. In general, mathematics uses exact Analytical Techniques while computers use approximate Numerical Techniques to solve a problem which is reflected in the nature of their proofs.
Coming to DbC, since it is based on Hoare Logic (i.e. an algebra with axioms/inference rules), a Program is written as a series of Preconditions/Postconditions/Invariants with the Programmer acting as the Proof deriver. Thus if a series of pre/post/inv holds at a certain stage in the program (i.e. proof) the next post will hold (barring external cataclysms). The fact that the proof obligation is discharged dynamically at runtime is immaterial. But we may not want that in certain categories of real world programs since the question of what to do when the proof obligation is not met at runtime becomes a problem; Do we abort/Do we rollback to older known state etc. For a CRUD app we can abort and have the user restart but for a heart pacemaker app we don't want that. In the latter case since it is a closed system with well defined inputs/outputs we can map DbC to VDbC and then prove it through a verifier statically thus guaranteeing invalid states can never arise at runtime. But note that this is merely an incidental distinction due to the needs of the real world but the essential DbC guarantees remain the same.
It should now be clear that when you map concepts from mathematical to computing domain you need to understand how the same names like "Integer", "Set/Type", "Algebra", "Axiom", "Proof" map from one to the other (though not exactly) and how you can leverage their isomorphism to use symbolic Mathematics effectively in Programming while at the same time keeping in mind their differences due to real world computation constraints and limits.
References:
1) Mathematical Proof - https://en.wikipedia.org/wiki/Mathematical_proof
2) Computer-assisted Proof - https://en.wikipedia.org/wiki/Computer-assisted_proof In particular; see the "Philosophical Objections" section.
3) See also the book From Mathematics to Generic Programming by Alexander Stepanov and Daniel Rose to get an idea of how to map between mathematics and programming.
A proof of a program's correctness is mathematical in nature, it doesn't stand apart in some distinct non-mathematical realm. (Whether we call it computer science is of little consequence here.) The tools for generating such proofs tend to use SMT solvers.
It's true that C's int type, for instance, does not correspond to the mathematical integers, despite the name. It has its own arithmetic rules. So what? It's still mathematical in nature.
I think this is really a disagreement on phraseology though, nothing deeper.
> The reason is because Mathematics deals with ideal and abstract objects whereas objects in the real world (eg. a computer program) can only map to aspects of the ideal world and not in its entirety.
Programming languages can be modelled mathematically. Programs can be modelled mathematically. That's much of the point of formal methods.
Real computers are finite state machines. So what?
> any proof which uses the axiom of associativity for signed integers in a computer can never be as absolute and general as its counterpart in pure mathematics
Modular arithmetic is mathematics, just as arithmetic over integers is mathematics. Formal analysis of floating-point arithmetic, or of C-style signed integer arithmetic, may be of less interest to pure mathematicians, but both can be (and have been) analysed with proper mathematical rigour.
If someone really mistakes C's int type for the mathematical integers, or the float type for the reals, then they don't understand the first thing about programming.
> In general, mathematics uses exact Analytical Techniques while computers use approximate Numerical Techniques to solve a problem which is reflected in the nature of their proofs.
Sometimes we need to approximate the reals, sure, but there's nothing approximate about, say, mergesort. Similarly a proof of its correctness (whether in the abstract, or of a particular implementation in a programming language) isn't in any way approximate.
> Coming to DbC, since it is based on Hoare Logic (i.e. an algebra with axioms/inference rules), a Program is written as a series of Preconditions/Postconditions/Invariants with the Programmer acting as the Proof deriver.
As I understand it, in typical design-by-contract software development, there is no formal proving of anything, there's just runtime checking.
It's possible to mistakenly believe we've come up with a model that is guaranteed to always preserve its postconditions and invariants. A decent introductory course on formal methods allows students to discover this for themselves, perhaps using Z Notation [0] or one of its derivatives. There's no substitute for proving your model correct.
If your starting point really is a proper formal model with a proof of correctness, what you're doing isn't typical design-by-contract software development.
> Thus if a series of pre/post/inv holds at a certain stage in the program (i.e. proof) the next post will hold (barring external cataclysms).
We only know that's the case if we've formally proven that the program is correct. If you're doing runtime checking, it's presumably because you don't know whether the program always does as you hope in all possible states.
> The fact that the proof obligation is discharged dynamically at runtime is immaterial. But we may not want that in certain categories of real world programs since the question of what to do when the proof obligation is not met at runtime becomes a problem [...] prove it through a verifier statically thus guaranteeing invalid states can never arise at runtime. But note that this is merely an incidental distinction due to the needs of the real world but the essential DbC guarantees remain the same.
It's not mere detail, it's an entirely different software engineering outcome. As you've just acknowledged, proving the absence of bugs from a codebase may be of life-and-death practical importance, and typically this cannot be achieved using runtime checks. A proof of correctness is a powerful assurance to have, and the tools needed to deliver it are radically different from runtime checks. It's in no way incidental, it's a whole different game.
Even if you were able to test your program on all possible inputs, which you can't, you still probably haven't achieved the equivalent of a formal proof of correctness. There are plenty of issues that runtime assertions are likely unable to provide assurances for. Does the code have a subtle concurrency bug, or read-before-write bug, or some other form of nondeterministic behaviour, such that it might have failed to arrive at the correct outputs, but we just got lucky this time? Absence of undefined behaviour? Absence of sensitivity to platform-specific or implementation-defined behaviours or aspects of the programming language, such as the maximum value that can be held in an unsigned int?
On the plus side, many of those issues can be mitigated by a well-designed programming language, or by compiler-generated runtime checks. The SPARK Ada language closes the door of many of them, for instance, whereas in C those sorts of issues are pervasive.
More generally, testing and runtime checking are able to discover bugs, but are typically incapable of proving the absence of bugs. This is much of the motivation for formal methods in the first place.
> when you map concepts from mathematical to computing domain you need to understand how the same names like "Integer", "Set/Type", "Algebra", "Axiom", "Proof" map from one to the other (though not exactly) and how you can leverage their isomorphism
Again I don't think it's helpful to phrase it as if there are 2 worlds here, one mathematical and one not. Program behaviour can be modelled mathematically. It's not math-vs-programming, it's just a matter of applying the correct math.
I'm not sure it's quite right to call it isomorphism, on account of computers being finite state machines. As you indicated earlier, computers can, roughly speaking, only cope with a subset of reality.
> A proof of a program's correctness is mathematical in nature, it doesn't stand apart in some distinct non-mathematical realm ... I think this is really a disagreement on phraseology though, nothing deeper.
It is mathematical in nature but if the objects it deals with do not obey the axioms and/or the axioms are inconsistent the whole edifice falls. You can provide a perfectly "valid" proof but starting with wrong/inconsistent axioms. In computing since everything is a series of calculations it becomes quite important to make sure that you can carry-over the axioms in an algebra "as is" from pure mathematics to programming. In the example that i gave, the C language gives you multiple sets (aka types) of integers (i.e. cartesian product of {signed, unsigned} X {8, 16, 32, 64}) which are all subsets of the mathematical structure Z. You can distribute these types across the variables a/b/c in the expression in many different orders each of which have to be proven separately for the axiom of associativity to hold generally.
> Programming languages can be modelled mathematically. Programs can be modelled mathematically. That's much of the point of formal methods. Real computers are finite state machines. So what?
Mathematics is static/declarative while Computing has both static/structural and dynamic/behavioural aspects both of which are amenable to mathematics but differently. This is the fundamental difference. It is also the reason so much of real world software is pretty good and correct in spite of not using any formal methods whatsoever. A "Proof" is simply a logical argument from {Premises} -> {Conclusion} whether done informally or formally. When we write a program we are the proof deriver logically moving from statement to statement to produce the desired result. This is "proof by construction" where we show that the final product (i.e. the program) meets the desired properties. By using Defensive Programming and Testing techniques we then "prove" at runtime that the properties hold. DbC is a more formal method of doing the same. TDD can also be considered as belonging to the same category.
> As I understand it, in typical design-by-contract software development, there is no formal proving of anything, there's just runtime checking ... We only know that's the case if we've formally proven that the program is correct. If you're doing runtime checking, it's presumably because you don't know whether the program always does as you hope in all possible states.
This is your fundamental misunderstanding. By "Formal" you are only looking at static verification of the program and ignoring all runtime aspects. DbC is formal verification at runtime of a proof you have hand derived statically using set theory/predicate logic as you write the program. It does not make it any less than other formal methods done statically (hence the easy mapping done to VDbC). It is the real world needs of the system which decides what is acceptable as pointed out previously.
There is also a movement towards "lightweight formal methods" where partial specification, partial analysis, partial modeling and partial proofs are deemed acceptable because of the value they provide.
> It's not mere detail, it's an entirely different software engineering outcome. ... More generally, testing and runtime checking are able to discover bugs, but are typically incapable of proving the absence of bugs. This is much of the motivation for formal methods in the first place.
No amount of Formal Methods application can help you against something going wrong in the environment (hence my use of the word cataclysm) and which directly affects the system eg. a EMP pulse corrupting memory, hardware failures etc. We mitigate against this using Redundancy and Fault-Tolerance techniques. Because in computing we have static and dynamic aspects we need to consider both as the field of use for Formal (and other) Methods.
> Again I don't think it's helpful to phrase it as if there are 2 worlds here, one mathematical and one not.
There absolutely is. It is the definition of Ideal vs. Real Worlds. In Computing you have the limitations of finite time, finite steps, finite precision, finite error/accuracy etc. It changes the very nature of how you would map mathematics to reality.
References:
1) Proof by Construction - https://en.wikipedia.org/wiki/Mathematical_proof#Proof_by_co...
2) Stackexchange and HN discussion Why is writing mathematical proofs more fault-proof than writing code? - https://news.ycombinator.com/item?id=16045581
3) When is a computer proof a proof? - https://lawrencecpaulson.github.io/2023/08/09/computer_proof...
4) The Central Dogma of Mathematical Formalism - https://siliconreckoner.substack.com/p/the-central-dogma-of-...
5) Lightweight Formal Methods - https://people.csail.mit.edu/dnj/publications/ieee96-roundta...
As far as I can see, that Wikipedia section doesn't connect to anything we've discussed.
We haven't discussed the impracticality of human verification of machine-generated proofs of properties of complex programs or models. We haven't discussed the possibility of bugs in verifier software.
> It is mathematical in nature but if the objects it deals with do not obey the axioms and/or the axioms are inconsistent the whole edifice falls.
Sure, but you seem to be stressing the risk of misapplication of mathematical axioms such as those of integer arithmetic, to contexts where they do not hold, such as arithmetic over int in the C language. As I've stated, formal methods are able to accommodate that kind of thing. We're both already aware of this.
You can formally reason about a program written in C, but naturally you need to be keenly aware of the way C code behaves, i.e. the way the C language is defined. You need to model C's behaviour mathematically. As you've hinted at, you need to account for the way unsigned integer arithmetic overflow is defined as wrapping, whereas signed integer arithmetic overflow causes undefined behaviour. The formal model of the source programming language essentially forms a set of axioms. Existing tools already do this.
> When we write a program we are the proof deriver logically moving from statement to statement to produce the desired result. This is "proof by construction" where we show that the final product (i.e. the program) meets the desired properties.
I'm not clear what software development methodology you have in mind here. It sounds like you're describing a formal methodology. It certainly doesn't describe ordinary day-to-day programming.
> By using Defensive Programming and Testing techniques we then "prove" at runtime that the properties hold.
These do not constitute a proof over the program.
> By using Defensive Programming and Testing techniques we then "prove" at runtime that the properties hold. DbC is a more formal method of doing the same.
No, again, that isn't proof in the sense of serious formal reasoning about a program. I guess it's a proof in the trivial sense, courtesy of the Curry–Howard correspondence, but I don't think that's what you're referring to.
In my prior comment I gave a list of reasons why runtime checking doesn't even necessarily prove that the program correctly implements a correspondence from the one particular input state to the one particular output state, as there's plenty of opportunity for the program to accidentally contain some form of nondeterminism such that it only happened to derive the correct output state when it actually ran. Program behaviour might be correct by coincidence, rather than correct by construction.
Consider this C fragment by way of a concrete example. I'll use undefined behaviour as the root cause of troublesome nondeterminism, but as I mentioned in my earlier comment, another would be race-conditions.
int i = 1 / 0;
int k = 42;
i = k;
Incorrect answer: i and k both hold 42, and execution can now continue. Variable i was briefly assigned a nonsense value by performing division by zero, but the last assignment renders this inconsequential.
Correct answer: undefined behaviour has been invoked in the first statement. This being the case, the program's behaviour is not constrained by the C standard, so roughly speaking, anything can happen. On some platforms it may be that i and k both hold 42, and that execution can now continue without issue, but neither is guaranteed by the C language. Nothing that occurs subsequently in the program's execution can reverse the fact that undefined behaviour has been invoked.
This is of course a trivial contrived example that's impossible to miss, but in practice, plenty of C programs accidentally rely on implementation-defined behaviour, and many accidentally invoke undefined behaviour, according to the C standard.
Putting lots of assertions into your code isn't an effective way of catching that kind of issue in practice. If it were, we wouldn't have so many security issues arising from memory-management bugs.
Even if all that weren't the case though, runtime testing still can't exhaustively cover all cases, whereas formal proofs can.
> TDD can also be considered as belonging to the same category.
No, that's really quite absurd. Try arguing to a formal methods research group that TDD is tantamount to formal verification. They'll laugh you out of the room.
> DbC is formal verification at runtime of a proof you have hand derived statically using set theory/predicate logic as you write the program.
For the reasons I gave above, it does not even definitively demonstrate the correctness of the code for a given input state, let alone in general.
Most people doing 'design by contract' are not starting out with a formal model expressed in set theory. I think you should find another term to refer to the methodology you have in mind here, it's confusing to refer to this as 'design by contract'.
You generally can't practically hand-derive proofs of properties of a large program or formal model, that's why computerised solutions are used.
> There is also a movement towards "lightweight formal methods" where partial specification, partial analysis, partial modeling and partial proofs are deemed acceptable because of the value they provide.
Sure, like I said earlier: I'm not opposed to the use of partial proofs or 'good enough' proof-sketches, both of which could be useful in producing high-quality software in the real world, but we should be clear in how we refer to them.
Something I should have added at the time: when using a formal software development methodology, it's possible, and likely necessary for practical reasons, to prove only a subset of the properties that constitute the program's correctness.
> No amount of Formal Methods application can help you against something going wrong in the environment
Of course.
> In Computing you have the limitations of finite time, finite steps, finite precision, finite error/accuracy etc.
Right, but do any of these defy mathematical modelling?
Limitations of that sort might make programs mathematically uninteresting, but that's almost the opposite of them being fundamentally irreducible to mathematics.
It is directly relevant to your misunderstanding of terms like "Proof" and "Formal". That and the various other references i had provided should give you enough information to update your knowledge. It is only when you start thinking at a meta-level (i.e. philosophical level) that you can understand them.
> Sure, but you seem to be stressing the risk of misapplication of mathematical axioms such as those of integer arithmetic, to contexts where they do not hold, such as arithmetic over int in the C language. ... The formal model of the source programming language essentially forms a set of axioms. Existing tools already do this.
Again, you have not understood my example at all. It has nothing to do with the C language but everything to do with axioms in mathematics mapped to any language. The fact that subsets of integer are represented as finite overlapping sets means their order of application in an expression (i.e. intersection) becomes significant and each order has to be proved separately which is not the case in mathematics.
> I'm not clear what software development methodology you have in mind here. It sounds like you're describing a formal methodology. It certainly doesn't describe ordinary day-to-day programming.
This is just normal programming where you explicitly think about the transformations of the state space where you execute the code mentally while moving from statement to statement. People do this naturally as they devise a algorithm. They just need to be taught how to formalize this using some rigorous notation after being shown the mapping to mathematical concepts.
> These do not constitute a proof over the program ... No, again, that isn't proof in the sense of serious formal reasoning about a program. I guess it's a proof in the trivial sense, courtesy of the Curry–Howard correspondence, but I don't think that's what you're referring to.
That is exactly what i am referring to. It is "proof in the trivial sense" and hence my mentioning defensive programming and testing techniques to go with the above. All programmers do this in the course of their everyday work and this is the main reason there is so much good software out there in spite of not using any formal methods. Note that the "correctness" of the final product depends to a large extent on the expertise/knowledge of the programmer.
> In my prior comment I gave a list of reasons why runtime checking doesn't even necessarily prove that the program correctly implements a correspondence from the one particular input state to the one particular output state, as there's plenty of opportunity for the program to accidentally contain some form of nondeterminism such that it only happened to derive the correct output state when it actually ran. Program behaviour might be correct by coincidence, rather than correct by construction.
I had already pointed out the static/structural and dynamic/behavioural aspects of a program and how you can map between and use the two. You can give specifications statically (eg. Typing) but verify them either statically (eg. total function from one type to another) or at runtime (eg. partial function from one type to another).
> Consider this C fragment by way of a concrete example. ... This is of course a trivial contrived example that's impossible to miss, but in practice, plenty of C programs accidentally rely on implementation-defined behaviour, and many accidentally invoke undefined behaviour, according to the C standard.
This is not directly relevant here.
> Putting lots of assertions into your code isn't an effective way of catching that kind of issue in practice. If it were, we wouldn't have so many security issues arising from memory-management bugs. Even if all that weren't the case though, runtime testing still can't exhaustively cover all cases, whereas formal proofs can.
Again, your understanding is simplistic and incomplete. C.A.R.Hoare wrote a retrospective paper to his classic paper on Hoare Logic after 30 years which clarifies your misunderstanding Retrospective: An Axiomatic Basis For Computer Programming - https://cacm.acm.org/opinion/retrospective-an-axiomatic-basi...
Excerpts;
My basic mistake was to set up proof in opposition to testing, where in fact both of them are valuable and mutually supportive ways of accumulating evidence of the correctness and serviceability of programs. As in other branches of engineering, it is the responsibility of the individual software engineer to use all available and practicable methods, in a combination adapted to the needs of a particular project, product, client, or environment.
I was surprised to discover that assertions, sprinkled more or less liberally in the program text, were used in development practice, not to prove correctness of programs, but rather to help detect and diagnose programming errors. They are evaluated at runtime during overnight tests, and indicate the occurrence of any error as close as possible to the place in the program where it actually occurred. The more expensive assertions were removed from customer code before delivery. More recently, the use of assertions as contracts between one module of program and another has been incorporated in Microsoft implementations of standard programming languages. This is just one example of the use of formal methods in debugging, long before it becomes possible to use them in proof of correctness.
> No, that's really quite absurd. Try arguing to a formal methods research group that TDD is tantamount to formal verification. They'll laugh you out of the room.
No, a person who is educated in Formal Methods would know exactly in what sense i am using TDD as a formal method. Hoare in the above article gives you a pointer for edification.
> For the reasons I gave above, it does not even definitively demonstrate the correctness of the code for a given input state, let alone in general. Most people doing 'design by contract' are not starting out with a formal model expressed in set theory. I think you should find another term to refer to the methodology you have in mind here, it's confusing to refer to this as 'design by contract'. You generally can't practically hand-derive proofs of properties of a large program or formal model, that's why computerised solutions are used.
You have failed to understand what i have already written earlier. DbC is based on Hoare Logic which is axiomatic formal system using set theory/predicate logic. So when a programmer devises the contracts (preconditions/postconditions/invariants) in DbC he is asserting on state space which can be verified at runtime or statically by generating verification conditions which are fed to a prover.
I doubt that you really understand DbC so start with wikipedia (https://en.wikipedia.org/wiki/Design_by_contract) and then Meyer's OOSC2 (https://bertrandmeyer.com/oosc2/) for details. Finally, see Meyer's paper "Applying Design By Contract" (https://se.inf.ethz.ch/~meyer/publications/computer/contract...) for implementation advice.
> Sure, like I said earlier: I'm not opposed to the use of partial proofs or 'good enough' proof-sketches, both of which could be useful in producing high-quality software in the real world, but we should be clear in how we refer to them. Something I should have added at the time: when using a formal software development methodology, it's possible, and likely necessary for practical reasons, to prove only a subset of the properties that constitute the program's correctness.
I had already pointed out that you need to both define and understand Formal Methods broadly for effective usage. The fundamental idea is what is known as "Formal Methods Thinking" defined from basic to advanced where at each level you learn to apply formal methods appropriate to your understanding/knowledge at that level. Read this excellent and highly practical paper which will clarify what i have been saying all along in this discussion; On Formal Methods Thinking in Computer Science Education - https://dl.acm.org/doi/10.1145/3670419
> Right, but do any of these defy mathematical modelling? Limitations of that sort might make programs mathematically uninteresting, but that's almost the opposite of them being fundamentally irreducible to mathematics.
They both limit the applicability of mathematical models as-is and at the same time give you greater opportunities to extend the mathematics to encompass different sorts of behaviours.
Finally, to bring this to a conclusion, read Industrial-Strength Formal Methods in Practice by Hinchey and Bowen for actual case studies. In one project for a control system, a complete specification is done using Z notation which is then mapped directly by hand to C code. The proof is done informally with actual model checking/theorem proving only done for a very small piece of the system.
This is not really true, especially if you're involved with physics and robotics even just a bit like a do. Without mathematics, you won't understand a thing.
But It’s less about the particular field and more about the mindset for thinking about problems. That’s kind of like asking what your most used library functions are.
Being able to determine when a mathematical framing is useful and apply it is harder than knowing how to do the math. It requires deeper internalization of the concepts. So your experience is common.
You can often iterate to something that kind of works by adding epicycles. What you're left with is something that fails in rare cases you can't explain, is difficult to change (we don't touch that code), and is slow.
Compare a complex homegrown data store to a relational database like postgresSQL. Both get the job done, but one has significantly more conceptual clarity and reliability.
Being able to come across a hard problem and say, ok this is how to frame it and here is how to go about it, turns months of fiddling into a direct route.
That's a good example of what I said. Most software engineers don't develop new database management systems. They just use one. And if they merely use it, they don't need or benefit from nontrivial math. The math is abstracted away behind the intuitive SQL syntax.
If you're not interested in acquiring the kind of competency to develop new software, and are just interested in combining existing software, then you don't need a college degree.
I use predicates and sets quite often in daily programming.