Earlier quoted context omitted.
I you prefer readable proofs, try Isabelle or Lean.
Or TLA+.
Lamport's structured proofs... should be easier. But I haven't had enough experience to say.
My unusual hobby
121–130 of 157 posts
Re: My unusual hobby
#122Earlier quoted context omitted.
> Mathematicians don't just write down a proof and cross their fingers. 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.
There is a nice parallel between the legal profession and programming. Programmers write software in such a way that they try (if they're any good) to reduce the number of assumptions made and the number of bugs and the ambiguities in their code. Failure to do so results in undefined behavior, crashing code and in internet facing code in possibly being hacked. Lawyers write code into contracts. Good lawyers try to do…
I used to think the same thing, until I learned that there are entire chapters of contracts textbooks on how to use and manage ambiguities effectively. a well-written contract many times has intentional ambiguities meant to limit liability in certain cases, or to use as fodder in negotiations.
Re: My unusual hobby
#123Reminds me of Principia Mathematica, where the author (Bertrand Russell) needs 379 pages to prove that 1+1=2. [1] > "From this proposition it will follow, when arithmetical addition has been defined, that 1 + 1 = 2." —Volume I, 1st edition, page 379. [1] https://en.wikipedia.org/wiki/Principia_Mathematica
I heartily recommend Mathematics Made Difficult by Carl Linderholm.
https://en.wikipedia.org/wiki/Mathematics_Made_Difficult?wpr...
Imagine an introduction to math in that style.
Re: My unusual hobby
#124Cool post! The stuff about Curry-Howard was really interesting and relates to a question i have been thinking about. But I'm a novice when it comes to the theory of type systems or theorem provers. Maybe someone here can enlighten me? 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/inv…
We do have such languages. For example, Java has JML [1], C has the very similar ACSL, and a programming language like Idris has a type system that can express arbitrary logical propositions (there are various tradeoffs that may influence the choice between a rich type system a-la Idris or a rich contract system a-la JML, but many of the principles are the same). The problem is that we do not yet know how to make eff…
Don't forget Ada/SPARK and Dafney. The former probably has the most actual experience and documentation and the latter is pretty well integrated.
Re: My unusual hobby
#125Earlier quoted context omitted.
There is a nice parallel between the legal profession and programming. Programmers write software in such a way that they try (if they're any good) to reduce the number of assumptions made and the number of bugs and the ambiguities in their code. Failure to do so results in undefined behavior, crashing code and in internet facing code in possibly being hacked. Lawyers write code into contracts. Good lawyers try to do…
I've always wondered if it were possible to express legal things via code. I imagine that there's a lot of ambiguity that needs "filling in" by a human, but there must be some set of legal arguments that can be literally codified. 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 d…
On a flight to London, I once spoke with an intellectual property lawyer about my pet idea for machine-checked law, at least limited to the domain of contract law.
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.
Re: My unusual hobby
#126Earlier quoted context omitted.
If what you say is true, then this is one more reason for me to learn TLA+. 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?
Well, TLA+'s proof system, called TLAPS [1], is not an independent proof assistant, but rather a frontend, which uses the proof-assistant Isabelle, combined with various SMT and tableau solvers for proof-search (like Z3, Yices, Zenon) under the cover. 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. Th…
With verification systems like Frama-C and SPARK, which have similar difficulties, I like to think of it as playing "what do I know at this point" until the proof goes through.
Re: My unusual hobby
#127Earlier quoted context omitted.
It's pronounced like "cock". It's named after the animal, and that's how you say it in French. It's how people who use the tool say it.
Not really, the English word "cock" has a very different vowel than the French "coq" - https://youtu.be/bIraCzL3dtI?t=4s is a pretty fair exemplar. It's a lot more like the "o" in "joke". (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 see…
Perhaps more like "Coke"?
Re: My unusual hobby
#128> The CI system runs Coq on my code and prevents me from merging it into the master branch if there is a mistake.
How does one make Travis CI prevent a merge?
Re: My unusual hobby
#129thinking about this same topic there is probably amazing opportunities out there for programmer mathematicians. Don't get me wrong, of course there are quants and such for trading firms but intuitively I would think there are an amazing number of applications for this kind of advanced mathematical programming that seem relatively under utilized.
Re: My unusual hobby
#130Earlier quoted context omitted.
Fun aside: I'd love to see the reaction of an applied-math class, like an engineering class, in which the instructor after having introduced the course, says, "let's go through some math prequisites for this class" and essentially starts reciting something equivalent to Principia Mathematica (without mentioning what he's trying to prove, meaning in a bottom-up fashion), - "If A is true, and B is true, then C is true"…
Do that to any pure math class and they will similarly walk out. You need to know where something abstract like this is going to follow at all.
> You need to know where something abstract like this is going to follow at all.
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.