10 ms·
Coming Soon: Machine-Checked Proofs in Everyday Development
- haskellandchill 9y agoMy current reading list: - Fundamental Proof Methods in Computer Science - Handbook of Practical Logic and Automated Reasoning - Software Abstractions - The Little Prover Yes, currently I have Athena, OCaml, Alloy, ACL2 (via Dr Racket/Dracula) all up and running to work through the exercises in these books. I'm very skeptical anything will come of this, but it interests me and I can see the value. Hopefully the speaker's next book Formal Reasoning About Programs (https://github.com/achlipala/frap https://github.com/achlipala/frap) will be a nice next step, I have Certified Programming with Dependent Types but have not cracked it yet. Also keeping an eye on Verified Functional Algorithms (https://softwarefoundations.cis.upenn.edu/vfa-current/index.html https://softwarefoundations.cis.upenn.edu/vfa-current/index....).
- abecedarius 9y ago> The Little Schemer Do you mean The Little Prover?
- haskellandchill 9y agoYes! Thanks.
- meneame2 9y agoThree extra classics: * https://books.google.es/books?id=YseqCAAAQBAJ https://books.google.es/books?id=YseqCAAAQBAJ * http://www.concrete-semantics.org/ http://www.concrete-semantics.org/ * https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/
- adultSwim 9y ago+1 for Software Foundations
- Animats 9y agoIn ten years. That's where I thought we were in 1983 - ten years away.
- wolfgke 9y ago> In ten years. > That's where I thought we were in 1983 - ten years away. Obligatory xkcd: > https://xkcd.com/678/ https://xkcd.com/678/
- MikkoFinell 9y ago> Obligatory xkcd God I cringe every time someone posts that. It's like the "Big Bang Theory" of internet comics.
- AlexCoventry 9y agoI think ten years is an extremely conservative estimate, since he's giving real-world examples in the talk.
- throwaway2048 9y agoThey had real world examples of formally verified code in 1983 too.
- adamnemecek 9y agoCryptocurrencies and digital contracts are going to pump an insane amount of money into this.
- 20171026 9y agoI was thinking the same thing. I just got an Ethereum certification but I don't want to just develop Solidity contracts at an hourly basis that just get hacked after I leave. Would the resources in the original post be worth looking into to build secure contracts?
- Roritharr 9y agoI can only ask a question, since i've got no know-how about this. How would such a proof checker know the intent of the code of not having backdoor/insecurity? How do you define security in a logical sense?
- wolfgke 9y ago> How would such a proof checker know the intent of the code of not having backdoor/insecurity? How do you define security in a logical sense? As you surely know, there is no such thing as secure/insecure, but a set of properties that are considered in IT security, which might even not be fullfillable all at the same time. The exact words vary depending on the book, but a popular classification in a German standard reference on IT Security is General protection goals: - Integrity - Confidentiality - Availability Further goals are - Authenticity - Acountability - Non Repudiation - Sometimes Anonymity So you first begin to formulate your protection goals. Next you can begin to forumulate this in a logical sense. Again there can exist quite different axiomatic implementations of a general protection goal. But since you want to see examples: A common model in literature for integrity is the Biba model: https://en.wikipedia.org/wiki/Biba_Model https://en.wikipedia.org/wiki/Biba_Model Another common model for integrity is the Clark-Wilson model: https://en.wikipedia.org/wiki/Clark%E2%80%93Wilson_model https://en.wikipedia.org/wiki/Clark%E2%80%93Wilson_model The mathematical dual of the Biba Model is the Bell–LaPadula Model for ensuring confidentiality: https://en.wikipedia.org/wiki/Bell%E2%80%93LaPadula_model https://en.wikipedia.org/wiki/Bell%E2%80%93LaPadula_model A model that ensures that the access rules will be free of conflict of interest (this of cause involves privacy and integrity aspects) is the Chinese Wall Model: https://www.cs.purdue.edu/homes/ninghui/readings/AccessControl/brewer_nash_89.pdf https://www.cs.purdue.edu/homes/ninghui/readings/AccessContr...
- skybrian 9y agoWhat progress has been made recently in making writing proofs easier? Are there any research projects targeting mainstream programmers?
- misterHN 9y agoPaper and pencil are still state of the art, pick up a copy of A Shorter Model Theory by Hodges (1997) and hire someone to check your proofs (a.k.a. take a math course at a university). Writing proofs is quite easy. Who is going to check it?
- agentultra 9y agoPlenty of advances in logic and category theory have enabled dependently typed languages to be both theorem prover and practical implementation language. See Lean.
- vladf 9y agoI'm interested but "Lean programming languages" and its varieties are difficult to Google. Would you mind posting a complete reference?
- cf 9y agoI think this is a good application paper for Lean showing how you can use it to develop machine learning algorithms. https://arxiv.org/abs/1706.08605 https://arxiv.org/abs/1706.08605
- agentultra 9y agoSorry I forgot the link! https://leanprover.github.io/ https://leanprover.github.io/
- slack3r 9y agoCheck out Ur/Web (http://www.impredicative.com/ur/ http://www.impredicative.com/ur/). It has been used by a "mainstream programmer" to build a RSS feed reader.
- jpochtar 9y agoWe already have a basic form of machine checked-proofs in everyday code: type systems. Type systems encode and prove simple theorems like "f(x: int) -> int returns an int, if x is an int". Typescript and Mypy show us that these proof checkers don't need to be built into a language. Even better, they show that proofs can be over subsystems of a program, since Typescript and Mypy both allow for partial/incremental typing. We just need to extend these systems to support more complex theorems.
- earleybird 9y agoand you end up in the neighbourhood of Idris which is, I find, a pleasant experience when doing development
- bcherny 9y agoIncremental type systems are super interesting. Lots of work being done in the last 10 years that blurs the lines between static and dynamic typing (monkeytype, reticulated Python), types and values (via the triumph of inferred types), kinds and types (powerful trait systems like Scala's), and even values and code (code synthesis like magichaskeller, or excel's flashfill). A bit of self promotion, I touched on this in a recent blog post if you're interested in this sort of stuff: https://performancejs.com/post/hde6a33/JavaScript-in-2017:-Year-in-Review,-Predictions-for-2018 https://performancejs.com/post/hde6a33/JavaScript-in-2017:-Y...
- qznc 9y agoMachine checked useable compilers exist (CakeML, CompCert). Useable kernels exists (SeL4). A few people officially work as proof engineers. The future is here, but not evenly distributed. ;)
- haskellandchill 9y agoWere you able to find a position? You are qualified, but it's very competitive, few jobs and many PhD level candidates with experience.
- qznc 9y agoDid not try. I'm only looking in southern Germany and afaik nobody does that here.
- jondubois 9y agoMathematical proofs of code are not suitable for most systems. Even unit tests which don't involve proofs can be a problem sometimes because they lock down API inputs and outputs. It's already a major problem when a developer wants to change some code and they have to spend hours updating unit tests every time. When in small teams, heavy 100% coverage unit tests slow down productivity, possibly by 5x or 10x. I imagine that adding proofs as part of the unit test suite would further increase the productivity cost overhead by a massive factor. In software development, you should avoid treating the code like if it's special or perfect because it's not and it will need to be changed in the near future when requirements change (and they will always keep changing). So locking it down into a specific state with proofs all around it is a bad idea for the vast, vast majority of cases. We need more wisdom in software development and that means taking a step back, looking at the big picture and asking questions like what are the negative side effects of each new methodology that we are introducing into our projects? There are always downsides, and we're crazy to pretend that every fancy new methodology is a silver bullet.
- hmottestad 9y agoIt's hard to know the intent of a developer by reading their code. You could always add a bunch of comments, which would help, but in the long run you risk them getting out of date. My unit tests are basically "comments" for my code, that show me how the code is supposed to work. When I make changes, the tests will tell me if I broke the intentions of the initial developer. Sure, when doing big changes, just updating and maintaining the tests is a lot of work, but so would maintaining documentation and comments be. So we have less documentation and fewer comments, and more tests.
- jondubois 9y agoI find integration tests more useful for documentation because they show you how the system works at a higher level which is precisely what new developers need to understand. If the code itself is written properly then the individual classes and objects used throughout should be high cohesion and easy to read without needing any comments or tests. There are always cases where unit tests are important though like the parts of the code that deal with money. But there is no benefit in adding unit tests if you're building a standard chat system for example; integration tests are sufficient in that case. Also getting 100% test coverage is a complete waste of time if you don't actually test the right kinds of input and output parameters.
- crb002 9y agoWe already have them. It's called compiler type checks. Albeit having an SMT solver in your unit tests is nice too.
- UncleMeat 9y agoType checking is (usually) intraprocedural and flow insensitive. That's what makes it easy. The other stuff is harder.
- mcguire 9y agoGood talk! So, one question: Adam gives one example of a proof where the initial automation fails because it does not consider a theorem that was previously proved. He also gives an example of some complex code where the proof is too tedious to do without lots of automation. What happens when your complex code changes in such a way that you need some extra lemmas but don't know what they are?
- yaantc 9y agoIt's manageable in practice I believe, and Adam quickly shows a feature related to this in the demo. First, if some new features are added with associated properties, then some theorems/lemmas related to these properties will have to be added and proven. I don't think that part is problematic, because it's a "local" decision. This work is focused on the change. The possible problems come from the impact of these changes to existing results. If you need to go and make other changes all over the place it wouldn't be scalable. But then automation and coq hint database can help. In the demo example you referred to Adam adds the lemma as a rewrite hint, and then it's picked by coq automation elsewhere. That's how local changes can automatically be leveraged globally by proof automation in existing proofs, with no changes (ok, not always. But that limits the impact).
- ted_dunning 9y agoI think that the classic ironical demonstration of the limits of proof systems comes up with the fact that CoqIDE 8.7.1 crashes immediately on OSX if you try to cut or paste anything. The problem, it turns out that they included a new version of OCaml which was incompatible with the older version of GTK that was being used. Result: crash due to seg fault. We really need both proofs and pragmatics. Proofs can give us confidence in the fundamentals when used appropriately for the processor, or for consensus algorithms like Raft, or key parts of the OS. Tests and statistical analysis can give us confidence that we haven't overlooked something crucial. Some systems obviously aren't very appropriate for formal methods (take machine learning, for instance, there can be no formal spec for what a fraud looks like). There statistics and testing will have to suffice because we have clear value on average even if we cannot formally guarantee the system. Other systems are much more appropriate for formal methods. I should hope that a heart monitor, CPU, voting machine or aircraft flight management system will have substantial amounts of formally proved code (I know that I am dreaming with the voting machines; let's settle for getting it down on paper). I don't want to collect a statistical sampling of whether an airplane works as we iteratively work out the bugs and specs in an agile fashion.