My unusual hobby
stephanboyer.com
stephanboyer.com
This offhand comment (which we can all forgive) makes it seem like mathematics happens in a vacuum. I can understand the temptation to think that way, and I hope I can make it clear that this is not the case.
General theorems typically grow out of a set of representative examples of interesting behavior (unit tests, if you will), are judged by their relationship to other mathematical objects and results (integration tests), and are reviewed by other mathematicians (user acceptance tests).
Mathematicians don't just write down a proof and cross their fingers. The proof is often one of the last steps. There is a high-level intuition that explains why a theorem or proof sketch is probably true/correct before a formal proof is found. These explanations are usually compact enough to help one re-derive proof ("X doesn't have enough 'space' to fill Y, and Z tracks that gap", or something like that), but aren't formal enough to put into any formal logic system I know of.
By the way, I'm a big fan of your "Math ∩ Programming" articles. People who found my blog interesting will certainly think the same of yours: https://jeremykun.com/
On the flip side, this is exactly what a lot of lawyers do when writing contracts. Not necessarily maliciously or negligently, but it can still make for fun questions of interpretation when things don't go as expected.
Lawyers write code into contracts. Good lawyers try to do so by removing ambiguity where ever they can. Failure to do so results in court cases where that ambiguity is resolved, and in some cases will result in damage for the party that originally contracted them to write the code.
Neither lawyers nor programmers are legally liable for such fuck-ups.
Lawyers can be held liable if they do a horrible enough job. Likewise for programmers, and there are a lot of people advocating for strict liability for software defects in commercial products/services.
They can be but it rarely happens. The most likely outcome is that another lawyer (or even the same one) will send you another large bill to try to fix the problem. This too is roughly analogous to what happens in programming.
Being able to run test cases through such a construct would be immensely useful - for example, how would changes to health care law impact someone? They could have unit tests that compare different outcomes and make it easier to understand how a new law would change things. People could ask very precise questions about how things would impact them.
Say you own an apartment building with a view of the ocean and I own the plot directly between it and the ocean. I threaten to build a wall that blocks your building's view of the ocean unless you buy my plot for 10x more than its market worth. Should that be legal? Say you succumb to my demand. Should you be able to then sue me and recover the excessive payment? I think many would have the intuition that my threat should not be legal and any resulting contract not valid, since it was extracted by duress.
But how about Firefox selling its search bar to Google for billions of dollars, carrying the implicit threat to use a different default provider should Google not pay. That seems more fair than the previous example, but why?
And how do you formulate that difference into a hard rule, without relying on human beings' (i.e. judge and jury) intuitions of fairness and equity?
Here is what the Restatement of Contracts has to say:
(1) A threat is improper if
(a) what is threatened is a crime or a tort, or the
threat itself would be a crime or a tort if it
resulted in obtaining property,
(b) what is threatened is a criminal prosecution,
(c) what is threatened is the use of civil process
and the threat is made in bad faith, or
(d) the threat is a breach of the duty of good faith
and fair dealing under a contract with the
recipient.
(2) A threat is improper if the resulting exchange is
not on fair terms, and
(a) the threatened act would harm the recipient and
would not significantly benefit the party making
the threat,
(b) the effectiveness of the threat in inducing the
manifestation of assent is significantly
increased by prior unfair dealing by the party
making the threat, or
(c) what is threatened is otherwise a use of power
for illegitimate ends.
And look at (2)(c), "otherwise a use of power for illegitimate ends". What does that even mean? It's basically a surrender, acknowledging that it is impossible to formulate a rule ex ante that totally captures our notions of fairness as they should be applied in every possible situation.
My language is a little sloppy here. There are plenty of legal rules that lawyers would call bright-line rules. But they'll usually still fall short of something that can evaluated in software, as a programmer might expect of a rule so-described.
He explained some of the many reasons why that’s an exceedingly difficult problem. Together we reasoned that it would be possible to implement some degree of machine checking and automation, but that an expert human would always need to review the results, because it’s humans who interpret the laws & contracts.
What I found interesting was that this originally stated, but not proved, by Cantor. Then a few semi-flawed attempts at proofs were made (flawed in the sense that they relied on other axioms like choice, or that they had errors).
These are leading mathematicians, including Cantor, who basically invented Set Theory from scratch. And they went through many years of struggle to arrive at a proof of a result. Which you now learn in an introductory class.
It really put into perspective for me just how hard some of these things are, and made me feel less bad when I struggle with some mathematics.
According to Wikipedia this particular theorem was proved almost immediately (but not published) by Dedekind, and then 10 years later proved by a 19 year old student in Cantor’s seminar. It’s not clear whether more than a handful of people cared or worked on it in between.
As for Cantor being a leading mathematician of the day: most of the other mathematicians of his time regarded this whole mess to not be mathematics at all. Poincaré called Cantor’s set theory a “disease”. It wasn’t until several decades later that a broader group of mathematicians decided that roping in set theory allowed them to conveniently hand-wave away (“oh, the set theorists will take care of that part”) a lot of thorny questions, letting them get on with their work as they had before, but now with an deflective answer whenever anyone asked such questions. ;-)
Could there exist a language where these sorts of proofs become easier to write, because that language captures the problem in a better way?
"To give you an idea of what an actual proof looks like in Coq, below is a proof of one of the easier lemmas above. The proof is virtually impossible to read without stepping through it interactively, so don’t worry if it doesn’t make any sense to you here."
is why Coq is not one of my favorite tools.
A proof consists of two things: the "proof state"---a statement of what you know at a given point--and a sequence of "proof operations"---the manipaulations that move from one proof state to the next.
Most mathematical proofs you have ever seen have been presented as a list of proof states, with the operations either explained in comments or taken to be obvious.
Coq (and most other similar systems) present the proof as a sequence of proof operations, with the state invisible unless you're going through it in a Coq IDE.
On one hand, that's the same thing as a program: a Coq proof is a program for creating the proof. Unfortunately, on the other, I've never been able to read Coq proofs the way I can read programs. Probably a lack of experience, I guess.
On the other hand, Coq is a damn fun computer game.
I don't think it's a lack of experience on your part. I worked with some people at MIT who were far better at Coq than I was, and they admitted the same thing. Coq proofs are unreadable, even when all the hypotheses and variables are given thoughtful names.
But, as you found, Coq proofs are not meant to be read; they are meant to be stepped through. I'm not sure if there is really a better alternative: if the formal proofs were made easier to read, they'd probably be much longer. And they can already get quite long compared to traditional paper proofs.
I think the right strategy is to break large developments into small lemmas, such that each proof is short and borderline obvious (similar to structuring a computer program to be self-documenting). Also, more experienced Coq users heavily invest in proof automation (building "tactics" in Coq) to make proofs short and sweet. I don't have much experience on that front, though.
So, a proof would be a pure function, taking a number of assumptions as arguments, and in order to write this proof you must first pass proofs of the assumptions to it as arguments (and then you can reference these proven assumptions in the body of the proof when needed).
Putting aside their steep learning curve, formal proof methods do not guarantee that the code you've written is bug free. They only guarantee that the code follows the requirements you defined given the conditions you also set on your inputs. You can think of it as a mathematical proof of your postconditions will hold given that your preconditions are true.
And you know what? People do make mistakes establishing those preconditions and postconditions all the time, and the tool is not going to be of any help. You've proven your code, but it may not do what you actually wanted it to do.
During a lecture I saw a tenured professor, who was a well-respected mathematician and expert in Coq, make some rather obvious mistakes while establishing those preconditions and postconditions. His proof was valid but worthless.
When you add that writing those proofs is actually rather time consuming, you end up with a niche product with little real-world applicability, except possibly for safety-critical environments.
Take e.g. a redundant interlock system that disallows opening a chassis unless the power is off and you've inserted a special key. Useless on a juice press #cough#juiceroo#cough#, but very important on a 20 W UV laser.
Or a six-point safety harness. I'm not going to put them in my daily driver, but I wouldn't get into a racecar without them.
Verification != validation, and there is no technique on the "make better code" side that will help with the validation side, not proofs, not unit tests, nada.
On the other hand, there is a certain amount of benefit of "double entry bookkeeping"; having a statement of what it's supposed to do separate from what it actually does. And you get bonus points if they're linked so that you know what it does is what it says it does.
It may be that there is 'little real-world" applicability' for the full deal as things stand now. But things like fancy type systems are trying to continually push usability towards proofiness.
Your argument is very strange. We use type systems not because we think we'll write perfect code, but because we know it will reduce the likelihood of making mistakes in our code (at least, when that type system is sound).
It seems like you're against writing proofs that your code is correct because you think you'll do better. I have a very hard time believing that, seeing as you probably aren't writing your own assembly (that beats a compiler) most if any of the time.
A compiler though with a type system actually REDUCES your cost. So these are very different beasts.
The article actually alludes to this, linking to this: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
In short: I like both my type systems and my theorem proving without any involvement of Curry-Howard :D
When you also consider that performing these proofs takes a very significant amount of time, you end up with something with very limited applicability for the vast majority of software development scenarios.
That's all I'm saying. Please don't argue against a strawman.
People seem to always bring this up but what's better? Verified code is about as close as you're ever going to get to bug free.
If you're doing a large proof, getting the specification wrong and not eventually noticing while working on the proof isn't common. You'll likely have something that isn't provable and get proof goals that don't make any sense. I don't think it's a common problem for mathematicians either that they end up proving the wrong thing.
I haven't heard of any examples of complex verified programs where later someone found a huge flaw in the specification. It would be like writing a set of unit tests and a complex program that passed them which had behaviour that goes against what you wanted.
Look at
> https://www.krackattacks.com/
"The 4-way handshake was mathematically proven as secure. How is your attack possible?
The brief answer is that the formal proof does not assure a key is installed only once. Instead, it merely assures the negotiated key remains secret, and that handshake messages cannot be forged.
The longer answer is mentioned in the introduction of our research paper: our attacks do not violate the security properties proven in formal analysis of the 4-way handshake. In particular, these proofs state that the negotiated encryption key remains private, and that the identity of both the client and Access Point (AP) is confirmed. Our attacks do not leak the encryption key. Additionally, although normal data frames can be forged if TKIP or GCMP is used, an attacker cannot forge handshake messages and hence cannot impersonate the client or AP during handshakes. Therefore, the properties that were proven in formal analysis of the 4-way handshake remain true. However, the problem is that the proofs do not model key installation. Put differently, the formal models did not define when a negotiated key should be installed. In practice, this means the same key can be installed multiple times, thereby resetting nonces and replay counters used by the encryption protocol (e.g. by WPA-TKIP or AES-CCMP)."
I personally would consider this as a clear example of a huge flaw in a specification where a correctness proof was done on.
Awesome, thanks for the recent example. My point is people seem to always bring up that specifications may have flaws as if this makes verifying code pointless. The guarantee of correctness is still an order of magnitude better than e.g. using unit tests and I'd wager it isn't common that specifications are wrong in a critical way. It's difficult to make a mistake specifying that a program should not have buffer overflows and out of range errors for instance.
The WPA2 flaw is an example of a specification missing an important property as opposed to a property being described incorrectly. People seem to jump on the latter the most I find as if it's common.
If a specification misses an important property it is in my opinion by definition an incorrect description (in particular in this case when this missing property indeed leads to a security problem).
> I'd wager it isn't common that specifications are wrong in a critical way.
> People seem to jump on the latter the most I find as if it's common.
Let me present you an hypothesis: Currenly few things are really formally specified. And if it is done, there are usually very smart people behind the project. Which by definition makes it rare that they contain lots of critical errors. On the other hand, if these methods were applied "large scale" (i.e. also by much less skilled programmers who don't have a lot of deeper knowledge about more than basic computer science topics), the rates of errors in specification would be much higher and I believe this could become a not-that-uncommon topic.
Of course I nevertheless believe that if a lot more properties were formally specified and correctness proofs were done, the error rates of programs would nevertheless go down by magnitudes. But I don't believe that formal specifications and formal correctness proofs are a panacea. What I rather consider as sad is that it seems to be that if formal specification and machine-checked proofs were applied "by nearly every program", we actually slowly get out of ideas what kind of tools we can develop to decrease the error rates even more...
I agree that missing important properties is very bad, but incorrectly stating a property, writing a complex program that matches it and completing the proof all without noticing sounds unlikely to me.
> On the other hand, if these methods were applied "large scale" (i.e. also by much less skilled programmers who don't have a lot of deeper knowledge about more than basic computer science topics), the rates of errors in specification would be much higher and I believe this could become a not-that-uncommon topic.
Hmm, so from my experience, if you're having trouble writing correct specifications you quickly end up getting stuck when writing proofs. Your specification won't match your program and your program won't match your specification so you'll be unable to finish your proof. If you somehow luck out through this a few times, you eventually won't be able to prove something else because a previous specification/theorem is wrong.
> But I don't believe that formal specifications and formal correctness proofs are a panacea. What I rather consider as sad is that it seems to be that if formal specification and machine-checked proofs were applied "by nearly every program", we actually slowly get out of ideas what kind of tools we can develop to decrease the error rates even more...
Besides having machines read our minds, I'm not sure where you can go from formal methods except inventing languages that make specifications easier to accurately describe. When it's still a ongoing debate if strongly typed languages are safer than dynamically typed languages we have a very, very long way to go so this isn't an issue yet...
Code verified by legible proofs is safer than merely verified. The quality of the verification language matters, it's not only the programming language.
If the specifications are human legible though, why do you care if the proof (which is checked for you by the machine) is legible? The main point of formal methods is to remove any doubt there are errors in the proof so it's an order of magnitude safer than relying on a readable hand written proof.
If you want a formal proof that is as readable as a hand written proof, you'd have to rely on a lot of automation going on in the background as every proof step must be traced back to basic axioms so complete proofs are pretty much always going to verbose and unreadable.
Because it is a goal of any science not to make a correct model, but also to get a high-level understanding what this model is about. Feel free to call this high-level understanding "what it is really about a "meta-property" of the model, which we also would like to have.
"Better" is a slippery term. Code doesn't exist in a vacuum, but rather in an external world that has other constraints (e.g., time and budget).
If using formal proofs means that you go through one development cycle while your competitor is iterating three, four, or five times, your milkshake is going to be drunk.
Barring compiler errors (which despite frequent protestations here, you're highly unlikely to encounter in day-to-day coding) the output of a compiler is a 'verified' translation of your source code. This doesn't translate to any guarantee of correctness and neither do proofs.
I think you are mixing “bug” with “out of spec”. If you ask me to write a perfect chess program, you can’t say it’s a bug if it can’t play go.
Bad or incomplete requirements are a problem, but that’s a different problem from “bugs”.
Either way, for Coq programs, it sounds to me like specifying the preconditions is part of the implementation, so the term "bug" seems especially apt
This always comes up when formal methods are discussed, and I've never been able to understand this. The goal isn't really to create a 100% correct program, but to significantly reduce the chance of bugs.
And while writing pre- and post-condition is one way, another is to write global correctness propositions for the entire program that are easy to inspect for correctness (e.g, a two-line formula saying "the database is always consistent", or "no data is lost even if a node crashes"). Usually, these properties are verified not against the program itself, but against some high-level spec serving as a blueprint, and while there is no formal proof that the code follows the blueprint, the same is true for buildings, and blueprints can help a lot. Use those blue-prints alongside code-level pre-/post-conditions, and you have yourself a highly reliable piece of software.
The vision is to be able to verify those global correctness properties all the way down to the code (and even to machine code). This is called end-to-end verification, and has only been accomplished for programs of (very) modest size and complexity, and even then with great effort. But even without end-to-end verification, you can greatly increase your confidence in your program, at a cost that is not only affordable, but may even save you some money.
I prefer Isabelle myself, as I find its proofs more readable in a traditional mathematical sense. Coq however, is probably easier for most programmers to experiment with.
Just curious, what makes Isabelle easier to read? I haven't tried it.
The structure of Isar proofs then more closely resemble a traditional mathematical proof, with a formalisation close to natural language. You can see the example from Wikipedia:
https://en.wikipedia.org/wiki/Isabelle_(proof_assistant)
As you can see, the overall structure of the proof is clearer, and you have less dependency of seeing the proof state to understand the proof.
The downside to Isabelle is that it introduces a dual syntax, with certain sections written in quotes. There's more to learn syntax and concept wise, but I think it's worth the extra effort for a clearer proof.
EDIT: Linked to Wikipedia page for formatting.
But my first reading of this comment was as a wry response to the content of the parent comment.
And that is why natural language is not a formal system!
> "From this proposition it will follow, when arithmetical addition has been defined, that 1 + 1 = 2." —Volume I, 1st edition, page 379.
- "If A is true, and B is true, then C is true"
- "We know A is true, therefore if B is true, C must be true"
- "B is true if and only if D is true and E is true"
- ...
- Therefore C is true.
- (on and on and on for a whole hour).
Indeed, and do remind your audience from time to time about where you're going. Otherwise, your whole line of reasoning might become useless to someone who lost track of the point, or just didn't hear or grasp it the first time you said it.
https://en.wikipedia.org/wiki/Mathematics_Made_Difficult?wpr...
Imagine an introduction to math in that style.
(first precondition IMPLIES (second precondition IMPLIES (implication))
is inherently harder for me to understand than
(first precondition AND second precondition) IMPLIES implication
even though logically they are the same. The first version carries more mental overhead because it seems to indicate that there is some sort of hierarchy/assymetry to the two preconditions.
It's the same thing when I try to read a Haskell function type signature:
f :: a -> b -> c
f is a function taking a and returning (a function taking b and returning (c))
vs.
f is a function taking two parameters a and b and returning c
There is no hierarchy anyhow because the parameters can be swapped:
f' = \b a -> f a b
Curious to know if it's just me or there are others who experience the same.
I think I started with the same assumption that you have: the order or parameters is arbitrary. In functional programming, though, this is not the case. For example, the "map" function takes a function and a functor (you can think of a functor as a collection like a list if you aren't familiar with the term). The order is important because if I partially apply a parameter to "map" I get a completely different meaning.
If you partially apply the function to "map", then the result is a function that applies that function to any kind of functor. If you partially apply the functor to "map", then the result is a function that applies any kind of function to that specific functor. Because I can only partially apply the first parameter in the function, this helps define the meaning of the function. In this example, the first definition is more correct (because "map" always takes the function first and the functor second). This becomes increasingly important as you build applicatives and monads.
In case that was unclear, here's a quick example. Let's say I have a list of integers and I have a function that adds 5 to an integer. If I do something like "map addFive list", it will go through each element in the list and add 5, resulting in a new list. If I partially apply the function to map with "map addFive", this will return a function that loops through any list and adds five to each element. So I might say "let addFiveToEach = map addFive".
If we had a different kind of map function (let's call it "mapNew") maybe we can do "mapNew list addFive" and it will do the same as the "map" code above. But if I partially apply list to mapNew I get a function that applies a function to my specific list. I might do "let eachInList = mapNew list".
The result is two very different functions. Either I will do "addFiveToEach list" or I will do "eachInList addFive". What meaning I prefer depends on the situation.
It's this idea that partially applied functions have a meaning that is powerful. When you are writing the code, which meaning do you want? As you note, both are possible, but I think you'll find that only one is actually appropriate in most cases. For example, instead of calling the function with both parameters, what if you assigned the result of partially applying the function to a variable? What would the variable be called? Does that help the reader understand the code?
Like I said, I was surprised at how often it makes a difference in my code. In fact, where it doesn't make a difference, it's usually an indication that I've made a mistake somewhere. It is even to the point where you start to want to pass partially applied functions around because they are more meaningful than the data that they contain. In fact a function is literally just another container in a functional programming language. For me, that was a kind of mind blowing realisation.
That's an artifact of the language, not inherent to functional programming.
(I had a longer response in mind, might write it up later when I get time.)
It does sacrifice some use cases, such as not knowing the total number of parameters, and does add more line noise. But I would be pretty happy with this tradeoff.
As someone with "journalistic" (but fairly in-depth) knowledge about these topics, my guess is that something like a proof-assistant will have to be paired up with some kind of logic programming system (like Prolog, or a kanren-derived system or something).
I guess then the problem of combinatorial explosion in logic search translates directly to the combinatorial explosion of proof-steps in a proof assistant. Hence my mention of partially-automated (more doable than fully-automated).
Probably some kind of a "database of facts" would also be involved, making it an expert system (reminds me of metamath [1]).
Is it fair to say, partially-automated theorem proving is a fairly advanced version (and not without added complexity) of a proof-assistant, and will help ease some of the grunt work involved in using a proof-assistant by hand?
I guess if I could simplify my discussion to one question, it would be: Does metamath or ghilbert use a logic inference engine to automate parts of a proof?
The way I understand metamath (the website, not the language) is that it's like an encyclopedia of mathematical knowledge. The encyclopedia is in the form of theorems, lemmas, corollaries, and their proof. But unlike an encyclopedia or disconnected articles, all the propositions build on top of one another. As a result, it builds (or tries to build) the whole mathematical edifice starting from core axioms (well, I guess it didn't build itself, but hundreds of mathematicians contributed to the database, like people contributing to wikipedia in the form of article-writing. As to how automated this process is, I don't know).
Now the question is, can we use this edifice as a database, to be input to a logic inference engine. What this would accomplish is that:
- If I make a query about a mathematical proposition (e.g., Are there infinite prime numbers), the logic inference engine would use the database to conclude that there are if it is able to access all the relevant propositions.
- If it's not able to reach a conclusion, e.g., if my query was "Are there infinite twin primes?" it would start a process of exploring new propositions from old propositions. Then either the search would conclude very quickly (if the proposition is only one or two steps away from the knowledge in the database) or it would give up after a few million, or billion attempts (e.g., this is more likely the case with the twin prime query). There will have to be a manually-specified cutoff point otherwise it could go into an infinite loop (I guess it may have something to do with decidability, incompleteness theorem, halting problem, etc, etc. Though even many decidable problems are computationally intractable due to very very large search space).
- Suffice to say, when I say "query" I don't mean a question in english language but a well-crafted mathematical statement in language of metamath itself.
P.S.: As for your mention of this work not doable as part-time, I fully agree with you. It would have enough cognitive load to be a very complex project even if done full time.
One of the interesting things about Metamath is that proofs tend to be very concise. In more automated proof systems, you use automated tactics and proof search techniques, and if you expanded out their output, they'd generally be quite verbose. I think this has led a lot of people to believe that automation is more necessary than it actually is.
All that said, you absolutely could build an inference engine of similar scope as the other big proof assistants, and use the existing Metamath database as a rich foundation.
Happy to answer other questions.
One key ingredient is the presence of a logic inference engine (and not for type inference only, as in Coq, Haskell).
- If your system doesn't have a logic inference engine, it's a vanilla proof-assistant (Coq).
- If it has one, it's one of two:
- a partially-automated theorem prover, (Isabelle)
- a fully-automated theorem prover
Here's a short video intro about MPE that I made: https://www.youtube.com/watch?v=8WH4Rd4UKGE
The thing I like about Metamath is that every step is directly visible. Coq, in contrast, shows "how to write a program to find a proof" - and not the proof itself. So you can see absolutely every step, and follow the details using simple hyperlinks.
Of course, all approaches have pros and cons. Metamath has some automation; the metamath and mmj2 programs can automatically determine some things, and there's been some experiments with machine learning that are promising. However, Coq has more automation, in part because it operates at a different level.
As type systems become more complex (like say in Scala or Haskell), they move towards having specialized syntax and weird hacks to express what are arguably simpler logical theorems/invariants about values in a type.. so why can't we have a programming language that gives you a full blown logic system(Coq? or Microsoft Z3? a SAT Solver?.. i don't understand the differences in detail) rather than part of one? Are there attempts at that, or does it turn out to be unworkable?
Most dependently typed programming languages, including Coq, give you the ability to basically "do logic" in a mostly unrestricted way.
There are a few challenges that come to mind with making a practical programming language that can also do arbitrary math:
a) For the language to be useful for proving things, it needs to be strongly normalizing. That means all programs halt—otherwise, you could trivially prove any proposition. Unfortunately that limits its utility as a general purpose programming language.
b) The languages which attempt to be useful for theorem proving are generally pure functional languages (due to the strong correspondence between functional programming and logic). Most programmers don't like working in pure functional languages, although the success of Haskell shows that there are certainly programmers who do (myself included).
c) The more expressive a type system is, the more difficult type inference becomes. Yet, paradoxically, I find myself writing more types in languages like C++ and Java than I do in equivalent Coq programs. I believe Coq uses a variant of a bidirectional type inference engine, which is quite usable in practice.
Idris is an attempt to make a practical programming language with the full power of dependent types. So it's probably the closest real language to what you're describing.
Z3 and other SAT/SMT solvers take a different approach: they try to search for proofs automatically, and for certain kinds of math they are very successful. But these are generally only for first-order theories or other restricted kinds of propositions, and not great for general theorem proving. They are good for things like proving array accesses are within bounds, or that you never try to pop from an empty stack (at least that's my understanding of their capabilities).
It doesn’t have some of the power of Idris’ elaborator reflection, for example, but it can eliminate many long-winded manual proofs via the SMT solver.
This is always mentioned and I always fail to see the relevance. Inferable terms stay inferable when we add dependent types.
Edit (too late to edit the original comment): After thinking about the kinds of type errors I've seen in my proofs, I think Coq's inference algorithm is based on unification (not bidirectional?). Whatever it is, it's quite nice to work with in any case.
It’s not true that a strongly normalising language must be limited in utility. See section 4 on codata of Turner’s 2004 “Total functional programmming” for more information.
https://github.com/mietek/total-functional-programming/blob/...
[0]: http://smallcultfollowing.com/babysteps/blog/2016/11/04/asso...
The problem is that we do not yet know how to make effective use of such code-level specifications. Finding a cost/benefit sweet spot is not easy (I personally prefer the JML approach precisely because I think it allows for greater flexibility in the choice of tradeoffs vis-a-vis confidence vs. cost).
When finally a type system becomes so expressive as to be Turing complete, you get 'undecidable types'. Those are the types that correspond to undecidable programs for Turing machines.
A consequence is that any `sound' typing system will have to reject some programs that actually are `well typed'. This is why many type systems have a "Just trust me, this is fine" option. Like casting in C/C++ and unsafe in rust.
To fully eliminate those "Just trust me" and still accept all well typed programs you'd need to accept potentially never ending type-checking (or else you'd have solved the halting problem).
I wonder if simplified versions of these proofs couldn't be used with students. Right now it seems like too much details, but maybe there can be a common "stdlib" of standard math arguments that we assume to be true, and then focus on the specific machinery for each proof?
It would seem to me that, if you're filling in details from an existing proof or making some existing formal (in the math sense) intuition more formal (in the Coq sense), there's not much deep insight to gain from implementing a proof in Coq.
For the domain theory proof I discussed in the article, formalizing it in Coq absolutely helped me understand it because:
a) Merely formalizing the definitions was valuable for me, because there are tricky subtleties to them (e.g., the supremum of a subset doesn't need to be in the subset, the various ways to define a "complete partial order", etc.).
b) When you do a formal proof, you have to refer to the definitions quite often. This just reinforces them in your brain.
c) Of course, when you formalize things in Coq, any misunderstandings you had about the material will be brought to your attention when your proof doesn't work.
On the other hand, I didn't gain much insight from the soundness proof for the simply typed lambda calculus. The definitions for that development were more straightforward. But I was already fairly familiar with the ideas of progress, preservation, etc. so I didn't expect to learn much from doing that. If anything, the main thing I gained from that was experience using Coq.
Such tasks are called "orienting tasks" in the cognitive science/human learning literature, and are useful because what it means to "understand" something is quite nebulous and we often fool ourselves when we actually think we understand something. They also allow us to test understanding outside of the domain it's supposed to be applied in, which is useful if the real situation is noisy, messy or costly.
Scott H Young explains the psychology of the problem well: https://www.scotthyoung.com/blog/2017/06/13/how-much-do-you-...
I love the format that the article takes, as well. I liked the superscript note numbers that xkcd's whatif blog uses, this is another implementation of that, executed very well.
I took the liberty of translating your module to TLA+, my formal tool of choice (recently, I've been learning Lean, which is similar to Coq, but I find it much harder than TLA+). I tried to stick to your naming and style (which deviate somewhat from TLA+'s idiomatic styling), and, as you can see, the result is extremely similar, but I guess that when I try writing the proofs, some changes to the definitions would need to be made.
One major difference is that proofs in TLA+ are completely declarative. You just list the target and the required axioms, lemmas and definitions that require expanding. Usually, the proof requires breaking the theorem apart to multiple intermediary steps, but in the case of the proof you listed, TLA+ is able to find the proof completely automatically:
LEMMA supremumUniqueness ≜
∀ P ∈ SUBSET T : ∀ x1, x2 ∈ P : supremum(P, x1) ∧ supremum(P, x2) ⇒ x1 = x2
PROOF BY antisym DEF supremum (* we tell the prover to use the antisym axiom and expand the definition of supremum *)
LEMMA natDiff ≜ ∀ n1, n2 ∈ Nat : ∃ n3 ∈ Nat : n1 = n2 + n3 ∨ n2 = n1 + n3
PROOF OBVIOUS (* this is automatically verified using just built-in axioms/theorems *)
Here's the module (without proofs, except for the one above):
------------------------------- MODULE Kleene -------------------------------
EXTENDS Naturals
(*
Assumption: Let (T, leq) be a partially ordered set, or poset. A poset is
a set with a binary relation which is reflexive, transitive, and
antisymmetric.
*)
CONSTANT T
CONSTANT _ ≼ _
AXIOM refl ≜ ∀ x ∈ T : x ≼ x
AXIOM trans ≜ ∀ x, y, z ∈ T : x ≼ y ∧ y ≼ z ⇒ x ≼ z
AXIOM antisym ≜ ∀ x, y ∈ T : x ≼ y ∧ y ≼ x ⇒ x = y
(*
A supremum of a subset of T is a least element of T which is greater than
or equal to every element in the subset. This is also called a join or least
upper bound.
*)
supremum(P, x1) ≜ ∧ x1 ∈ P
∧ ∀ x2 ∈ P : x2 ≼ x1
∧ ∀ x3 ∈ P : ∀ x2 ∈ P : x2 ≼ x3 ⇒ x1 ≼ x3
(*
A directed subset of T is a non-empty subset of T such that any two elements
in the subset have an upper bound in the subset.
*)
directed(P) ≜ ∧ P ≠ {}
∧ ∀ x1, x2 ∈ P : ∃ x3 ∈ P : x1 ≼ x3 ∧ x2 ≼ x3
(*
Assumption: Let the partial order be directed-complete. That means every
directed subset has a supremum.
*)
AXIOM directedComplete ≜ ∀ P ∈ SUBSET T : directed(P) ⇒ ∃ x : supremum(P, x)
(*
Assumption: Let T have a least element called bottom. This makes our partial
order a pointed directed-complete partial order.
*)
CONSTANT bottom
AXIOM bottomLeast ≜ bottom ∈ T ∧ ∀ x ∈ T : bottom ≼ x
(*
A monotone function is one which preserves order. We only need to consider
functions for which the domain and codomain are identical and have the same
order relation, but this need not be the case for monotone functions in
general.
*)
monotone(f) ≜ ∀ x1, x2 ∈ DOMAIN f : x1 ≼ x2 ⇒ f[x1] ≼ f[x2]
(*
A function is Scott-continuous if it preserves suprema of directed subsets.
We only need to consider functions for which the domain and codomain are
identical and have the same order relation, but this need not be the case for
continuous functions in general.
*)
Range(f) ≜ { f[x] : x ∈ DOMAIN f }
continuous(f) ≜
∀ P ∈ SUBSET T: ∀ x1 ∈ P :
directed(P) ∧ supremum(P, x1) ⇒ supremum(Range(f), f[x1])
(* This function performs iterated application of a function to bottom. *)
RECURSIVE approx(_, _)
approx(f, n) ≜ IF n = 0 THEN bottom ELSE f[approx(f, n-1)]
(* We will need this simple lemma about pairs of natural numbers. *)
LEMMA natDiff ≜ ∀ n1, n2 ∈ Nat : ∃ n3 ∈ Nat : n1 = n2 + n3 ∨ n2 = n1 + n3
(* The supremum of a subset of T, if it exists, is unique. *)
LEMMA supremumUniqueness ≜
∀ P ∈ SUBSET T : ∀ x1, x2 ∈ P : supremum(P, x1) ∧ supremum(P, x2) ⇒ x1 = x2
PROOF BY antisym DEF supremum
(* Scott-continuity implies monotonicity. *)
LEMMA continuousImpliesMonotone ≜ ∀ f : continuous(f) ⇒ monotone(f)
(*
Iterated applications of a monotone function f to bottom form an ω-chain,
which means they are a totally ordered subset of T. This ω-chain is called
the ascending Kleene chain of f.
*)
LEMMA omegaChain ≜
∀ f : ∀ n, m ∈ Nat :
monotone(f) ⇒
approx(f, n) ≼ approx(f, m) ∨ approx(f, m) ≼ approx(f, n)
(* The ascending Kleene chain of f is directed. *)
LEMMA kleeneChainDirected ≜
∀ f : monotone(f) ⇒ directed({ approx(f, n) : n ∈ Nat })
(*
The Kleene fixed-point theorem states that the least fixed-point of a Scott-
continuous function over a pointed directed-complete partial order exists and
is the supremum of the ascending Kleene chain.
*)
THEOREM kleene ≜
∀ f : continuous(f) ⇒
∃ x1 ∈ T :
∧ supremum({ approx(f, n) : n ∈ Nat }, x1)
∧ f[x1] = x1
∧ ∀ x2 : f[x2] = x2 ⇒ x1 ≼ x2
=============================================================================As I asked in a different question, is TLA+ able to do the proofs declaratively and automatically because it has an internal 'logic inference' engine?
Isabelle and Lean also make use of automatic provers for proof automation.
BTW, TLA+-style declarative proofs are not always better than Coq-style imperative proofs. They are certainly easier to read (the proof language was designed to be easily readable by humans), but they're sometimes harder to write, because it's largely an iterative trial-and-error process: you first try to prove the entire proposition automatically. If it fails, you look at the error message, try to see the difficulty, and then break the proof down into smaller steps, and so on.
I'd say it still appears to be better than fully-impertive "manual" process. (though I have used neither Coq nor TLA+).
- In Coq, you have to construct the whole proof yourself. Coq system merely verifies what you constructed.
- In TLA+, you need to do 1 or more iterations, but you have the full-weight of the computation behind you, sharing your cognitive load. Your only cognitive load is to think about the critical parts of the proof, if any, and the system will do the rest.
I wonder if the TLA+ system also uses a "database of propositions" behind the scenes to help with faster inference, e.g., something equivalent to Russell and Whitehead's Principia Mathematica (but in a coded form), or like metamath.
I really don’t know. It may largely depend on what you want to do, and I believe Coq also has powerful proof automation, albeit one that works differently. Both take quite a bit of practice to write. The main thing I can say is that TLA+ proofs are easy to read. In any event, formal proofs in any style are far from a walk in the park (which is why when using TLA+ in practice we try to avoid them altogether and just use the model-checker).
Also, TLA+ is a much gentler introduction to formal methods, as it's so, so, so much easier to learn, and the availability of a model checker means that, when learning, you can concentrate on writing specifications, a much more important skill than writing proofs (if you're interested in software, that is).
> I wonder if the TLA+ system also uses a "database of propositions" behind the scenes to help with faster inference, e.g., something equivalent to Russell and Whitehead's Principia Mathematica (but in a coded form), or like metamath.
It automatically uses the axioms of the core logic (essentially ZFC set theory with a Hilbert's choice operator, some simple theorems on the built-in sets, like the natural numbers [0] plus TLA, which is a simple yet very powerful temporal logic for computational reasoning). Other than that, it is a core principle of the system that you manually list which theorems are to be used for each step of the proof. It doesn't only help the provers -- it also helps the human reader. But, to save you typing, you can write "USE lemma1, lemma2", and have them automatically added to all following steps.
The proof language (like the entire specification language) was designed mostly by Leslie Lamport, based on his "structured proof" style detailed here [1]. The appendix of the paper lists some formal calculus proofs, checked with TLAPS, if you want to get a sense of what those proofs look like.
[0]: For example, here's the proof for the natDiff lemma from the post:
LEMMA natDiff ≜ ∀ n1, n2 ∈ Nat : ∃ n3 ∈ Nat : n1 = n2 + n3 ∨ n2 = n1 + n3
PROOF OBVIOUS (* this is automatically verified using just built-in axioms/theorems *)
But it’s very important to know that TLA+ has very different usage goals from Coq/Lean/Isabelle, and so makes very different design tradeoffs. The tools are certainly not interchangeable.
Coq, Lean and Isabelle are first-and-foremost research tools. As such, they are completely general purpose, very powerful, but also very, very complicated. TLA+, on the other hand, was designed for use by ordinary engineers to specify and verify large, real-world digital (software or hardware) systems. This means that TLA+ is not generally appropriate for doing high math (e.g., because it’s untyped, it doesn’t even have operator overloading, which alone would make it unappealing for serious math; then again, not much serious math is done formally, anyway), and isn’t designed for logicians to explore various logics (it’s classical logic only). In addition, it’s syntactic/symbol manipulation capabilities are very limited, so while you could specify a programming language, as you’ve done, the result is going to be much messier (although specifying low-level languages with simple syntax, like machine- or byte code, can be very elegant).
OTOH, TLA+ is truly exceptional in its ease of learning and its capabilities when it comes to specifying and verifying systems and algorithms. In many respects, it’s computational theory is richer than Coq’s (although Coq is so general that some people have embedded TLA, the computational theory of TLA+ in Coq; but TLA+ has it out of the box). In addition, when used in industry, people hardly ever use TLA+’s proof system. Not because it’s inadequate for proving the correctness of algorithms — it truly excels at that — but because formal proofs are, in general and regardless of the choice of tool, not very cost effective. Instead, TLA+ has a model checker that lets you verify your propositions about your system completely automatically — you just state them and press a button — albeit, only on small, finite instances. This is more than sufficient for industry use, as, while there have been multiple cases of informal (published and peer-reviewed) correctness proofs later found to be wrong with a model-checker, I am not aware of any cases where a model checker result was found wrong, despite running on small instances, and so not qualifying as proof.
So the choice between TLA+ and Coq/Isabelle/Lean is usually simple. If you’re an academic researching new logics, new programming languages, or complex formal mathematics, you’ll choose Coq/Isabelle/Lean. If you’re an engineer trying to design a complex or subtle system or algorithm, you’ll likely choose TLA+.
I can think of a few languages that started from a formal theory (e.g., Eff [1]), but none of them are "mainstream". There was a mostly successful attempt [2] at formally specifying C and implementing a verified compiler for it. Standard ML has a very comprehensive spec [3], perhaps the best of any "mainstream" language. It's not quite at the level of a Coq formalization, but also not too removed from it. Haskell is based on a lot of peer-reviewed papers, but there isn't one comprehensive spec for it at this level of formalism. Also, the RustBelt project [4] is worth mentioning. It's an initiative to develop a formal theory of Rust.
> If someone is interested in creating a new programming language, is it worth getting up to speed on proof writing and using that to build the language?
If your new programming language contains a novel idea that you want to have published in a peer-reviewed journal/conference, then yes, I think it is absolutely worth it. It's likely your paper will be rejected without having formal proofs.
But if you don't intend to publish your ideas, it's really quite a lot of work and might not be worth it. Depends on how dedicated you are, and how much you care about things like soundness.
It leads me to speculate... what if I don't need types to write correct software? I assumed I would implement typing and type inference (like Factor language already has) at some point. But if the code has no bugs without it... YAGNI?
My reasoning goes like this: Let's postulate that we have a library of functions, each of which has the quality Q of being error-free. If we derive new functions from the existing ones by a process that preserves Q, so that new functions are all also error-free, then we cannot have errors in our code, just user error. I.e. the user can present bad inputs, but no other source of error exists (other than mechanical faults.) This would be a desirable state of affairs. Now if the Q-preserving new-function-deriving process doesn't require types to work, then we don't need them. Whether or not typing helps prevent user error is another question. Personally, I lean toward defining user error as UI error, but I am ranging far from my original point now.
(If you're interested: https://github.com/calroc/joypy/tree/master/docs Still very DRAFT versions. https://github.com/calroc/joypy/blob/master/docs/3.%20Develo... )
It's almost like you get the bad side of programming (time-consuming, tedious) without the reward (seeing your program doing cool things). And you don't get the satisfaction of doing maths either. At least I don't. Maybe I didn't try hard enough.
What is very interesting though is to learn about type theory and the Curry Howard isomorphism.
1) The underlying pure functional language that forms the logical basis for Coq (called "Gallina"). It is not possible to write a program which runs forever in this language, because all recursive calls must be "well founded". Coq uses a very simple set of rules to determine when recursive calls are guaranteed to terminate (slightly more flexible than primitive recursion), but it rules out some legitimate programs which do not terminate. For example, writing merge sort is difficult in Coq because the type checker can't automatically prove that the recursion terminates. For these cases, you can provide your own ordering relation and prove that it is well-founded. So tldr, you have to prove that your programs terminate (and this is automated in many cases). The fact that all Gallina programs terminate is crucial; otherwise, you could trivially prove any proposition.
2) Usually in Coq you do not write most proof terms in Gallina manually (because it is quite unnatural). Instead, you write scripts called "tactics" to generate the terms for you. These scripts are written in a dynamically typed language called Ltac, and programs in this language can run forever. But all proofs generated by these tactics are type checked in Gallina, so it's impossible for a tactic to generate a bad proof term without it being detected by Gallina's type checker.
(Typo, but too late to edit the original comment.)
Coq's logic is intuitionistic, which means it's impossible to prove the following: forall P, P or ~P. But this actually makes Coq more powerful than classical logic, not less, because:
a) If you want, you can add that proposition (called the law of the excluded middle) as an axiom. Now you have classical logic.
b) By not adding that axiom, you can show that certain results do not depend on it. You couldn't do this if it were built-in.
Coq is based on a logic system called the "Calculus of constructions" https://en.wikipedia.org/wiki/Calculus_of_constructions. As such it has the same limitations as that logical system.
Most notably, Gödel's incompleteness theorems place a limit on what's provable in Coq, or indeed many other systems.
There are various kinds of logic systems, each with different kinds of 'power'. Power is a double-edge sword in logic systems, as with power comes the capacity to introduce paradoxes and inconsistencies.
As with programming languages, certain logic systems and automated logics are suited for particular cases. For example, there is a system 'MetiTarski' like a Domain Specific Language, designed to prove theorems about real-valued special functions.(https://www.cl.cam.ac.uk/~lp15/papers/Arith/).
Like the proof that there are proofs incapable of being expressed in Coq?!
How does one make Travis CI prevent a merge?
(edit: maybe you're English? Some English accents of England would articulate "cock" very close to French "coq" and "joke" would be far away. Apologies, one really does need to specify which "English" is meant, and I should have seen that at once. First cup of coffee still in progress.)
In your example the 'o' is more precise and the 'k' is swallowed a little.
I'd expect they're different accents, perhaps your example is more Northern French (I really don't know).