14 ms·

Programming languages going above and beyond

338 points by rrampage 3y ago

snitty 3y ago
>function Gcd(a:nat, b:nat) : (g:nat,x:int,y:int)) I hope this is a typo. Otherwise it…requires an unmatched close paren? That's a new level of cursed syntax. EDIT: Also, is |array| a common way to get the length of an array in languages? I've never seen that (or some of this other syntax) before and it took me a minute to figure out what was happening.
- jbl 3y ago
  |array| looks like it’s taken from the notation for cardinality of a set (number of elements in a set)
  - snitty 3y ago
    That makes sense. I initially read it as "absolute value." Which, admittedly, doesn't make sense for an array, but is a reasonable interpretation at first blush.
- hdctambien 3y ago
  I don't know about programming languages, but in mathematics |v| is the notation to get the length of a vector... So maybe Matlab uses that syntax?
  - deleted 3y ago
    [deleted]
  - RGBCube 3y ago
    FYI, MATLAB uses `length(v)` to get the length of vector v.
- deleted 3y ago
  [deleted]
- redjamjar 3y ago
  > I hope this is a typo Yeah, sorry --- that is a typo.
artemonster 3y ago
I have a very bad opinion about this, why there were no quantum leaps in programming: in practical world there is just no time to think out of the box. its an endless crunch and race to ship, so something brand new and „risky“ can only be born out of strong vision and necessity. On the other hand if we take PL research - it is too far detached from practical reality. Have you ever tried grokking type proofs? It is driven by a separate breed of mathematicians that cosplay as programmers and they build their „perfect and sound“ (and useless) world. Do you know how many tons of (garbage) papers were in the era when AOP was the rage? What are the practical results? And where are they? Or take Haskell as an emple, where nobody can clearly explain to a java codemonkey what a goddamn monad is? Or endless continuations and effects research and formalisms by Felleisen and Kiselyov only for all of it be kinda rediscovered and slapped on by react devs? Useless, all of it.
- anonzzzies 3y ago
  Everyone can explain to everyone what a monad is for and how to use it. The fundamentals in category theory, you really don't need. But because it got such a bad name, everyone is afraid and believes it must be much harder than they think. Dependent types and other proofs are not that hard to understand in principle; you can be working on them for a very long and that indeed makes it mostly impractical. However, we will see some interesting things in search space limiting between program synthesis, verification and LLMs. I tend to prove only the parts that are vital and the things that come automatic (when the holes are automatically filled because they are already 'done').
  - c_crank 3y ago
    Explaining how to use a Javascript Promise is simple. Explaining how to write idiomatic pure code using Monads is hard, and impractical in most cases, despite what FP purists will tell you.
    - anonzzzies 3y ago
      Yes, that's true, but in general programming is not easy, especially when there is something at stake (so probably most professionally written software) and as i'm work as an enterprise troubleshooter mostly in banking/insurance/trading, the depressing amounts of javascript/typescript code I encounter that should never have been put in production, while I hardly ever encounter bad f#, ocaml, rust, haskell or c++ (modern versions). Sometimes it's not excellent, but it's never as bad as the vast majority of nodejs running projects. The programmers of the latter are far more rigid, because it's hard to do anything, but when you do, you get rewarded. People learn JS in 2 days, slap on :any and blam, typescript gurus, get a job, create a system that processes millions$ and then leave for the next 'adventure'. People who invest in rigidity create better software. But yeah, they are far thinner in the 'get shit done fast' arena. So yes, I agree, if you want something done quickly and don't mind if it expires a few months later, you don't grab haskell, rust and definitely not a dependently typed language or proof assistent.
Jeff_Brown 3y ago
I'm a believer too (in dependent types). Software already bears an ungodly amount of responsibility, and with AI it will only become more so. Correctness is critical. While tests are good, it's impossible yo cover every case. Compiler-verifiable properties are better.
- wredue 3y ago
  [flagged]
  - consilient 3y ago
    > who still cannot formally prove a linked list properly after decades. Huh? Prove what about a linked list? https://www.idris-lang.org/docs/idris2/current/base_docs/docs/Data.List.html https://www.idris-lang.org/docs/idris2/current/base_docs/doc... seems like a perfectly good dependently-typed linked list to me.
    - astrange 3y ago
      Which makes it useless, since despite their teaching-programming popularity, linked lists aren't actually good for anything. The useful kind is called intrusive linked lists, but nobody teaches those.
      - consilient 3y ago
        Intrusive linked lists trade away simplicity and ease of refactoring for better memory characteristics. There's a huge amount of code where that trade is a terrible deal. Obviously you shouldn't use ordinary linked lists deep in the guts of an OS kernel or automated trading system but claiming that they're useless is absurd.
        astrange 3y ago
        The main issue is that a list of pointers is inefficient but also overkill; a small list is probably fine as an array even if you're mutating it. But intrusive lists also have clearer ownership, since the object knows all the lists it can be in, and that's handy sometimes.
anonzzzies 3y ago
Hope people are not going to mention that this is a blockchain company. No matter how I don't like it; this work, research and others (like Wadler) is great and very interesting advancements in the software verification space. You can ignore the blockchain side of things.
- john-radio 3y ago
  > You can ignore the blockchain side of things. You can, but you don't have to...
- simpsond 3y ago
  Verification of onchain protocols seems like a great fit.
  - anonzzzies 3y ago
    It is, it advances this theory and tech. I only mentioned it because many people will simply not read anything that has blockchain associations.
    - classified 3y ago
      Blockchain is just a solution in search of a problem. It's the cryptocurrency stuff where it gets shady.
- hobofan 3y ago
  > Hope people are not going to mention that this is a blockchain company. Well, nobody apart from you did...
Arainach 3y ago
SAT solvers are fun. Math is fun. Neither is the most important part of development. Most of my time is not spent formally testing these methods; it is understanding how systems interact and their performance characteristics. I disagree with OP's assertion about legacy languages; they have largely focused their improvements on the areas that actually matter to my day to day development.
- anonzzzies 3y ago
  > it is understanding how systems interact and their performance characteristics. But there is, at least a theoretical, promise that when you are rigid enough in your types, you are able to predict & prove memory, cpu, network use etc. It's pie in the sky, especially for interacting systems, but there is some future to cling on to. When doing embedded work, I use some of these to make sure algorithms stay within the limits in a way that they won't compile if they don't. There are also provable security which I also use (sparingly). We will get there, hopefully before I give up coding and become a fultime carpenter.
  - AnimalMuppet 3y ago
    I think you are on the path that is how this will actually be used: It gets added in little bits. I could be rigid enough with my types to prove more than I do. I don't because the payback isn't worth the effort. When it is worth the effort, then people will (gradually start to) use it. > When doing embedded work, I use some of these to make sure algorithms stay within the limits in a way that they won't compile if they don't. Could you be a bit more specific here about what you do, why you do it in embedded (and not elsewhere), what it protects you from, and how it does so?
    - anonzzzies 3y ago
      > Could you be a bit more specific here about what you do, why you do it in embedded (and not elsewhere), what it protects you from, and how it does so? We create, upgrade, maintain, validate applets for emv and other cryptographic and sensitive embedded (MCUs) applications; I try to guarantee safety using tla+, coq, z3 and agda. Or just on paper. And we deliver that as paper with our software. It’s just some functions, not all: we often have to, because of certification, show ‘a story’ (not proof) that things will be ‘secure enough’. I personally enjoy it more to prove some of the crucial parts as ‘the story’ not write a story.
agentultra 3y ago
Dafny is a cool language. Conal Eliot, in his 2023 Zurihac talk, says that in order to get efficiency (faster computers that can do more with less) at scale (not merely resilience which we get by adding redundancy and operational tooling) we need languages and tools that allow us to precisely specify the correct program. Dafny is a good step in that direction. I’m also keen to see where the depedently typed programming languages like Lean 4 and Idris 2 will take us. Proof-carrying code could be very useful.
- practal 3y ago
  Thanks for pointing out the Conal Elliott talk. Just watched it, very nice talk. I found myself nodding to pretty much everything he said, except of his fondness for dependent types. Each time he says "dependent types", I just replace it in my mind with "logic". I think he will transition eventually: Types (Haskell) -> Dependent Types (Agda) -> Logic (Practal), hehehe.
  - agentultra 3y ago
    Well you can encode any logic you want in dependent types, so yeah probably!
    - practal 3y ago
      Fair enough. Although to encode a proposition as a type, only to then view it as a proposition again, would be two wrappers too many for my taste. I prefer to keep the notions of truth and types apart. In practice, this makes the logic both simpler and more expressive.
- sn9 3y ago
  Talk link: https://youtu.be/k6rY5Mvx84E https://youtu.be/k6rY5Mvx84E
TrueDuality 3y ago
This is pretty cool! I do have a nitpick I think is important. An empty byte array getting converted to zero seems like a bad edge case that should probably produce some kind of error invariant. This isn't a minor concern if the intent is to use this in serious applications that require this degree of formalism. The two proofs are easy to break: `ToBytes(FromBytes([])) != []`. It's an obvious example of the issue: FromBytes handles inputs ToBytes can't generate therefore they are not true inverses of each other. It's a simple case but it was quick to find in this simple example, and it hints at dangerous oversights that could lead to severe bugs in more complex scenarios, like in cryptography. It's critical to account for such edge cases.
- occamrazor 3y ago
  TFA makes exactly this point. The lemma that Dafny proves is true, the reversed one is not and Dafny can provide the counterexample (the empty list).
  - TrueDuality 3y ago
    I didn't notice that it is kind of called out in the post... It's the very last line and left as an exercise to the reader to infer which is almost worse since I would call this a flaw in the implementation of the functions and is being shown off as a sterling example of the capabilities of the language. The conversion between `[]` and `0` is the flaw that is hard to reason about here and propagates through any code that interacts with it in a way that violates a programmers expectations.
    - fluoridation 3y ago
      It's not that uncommon to have de/serialization functions where g(f(x)) == x for all x, but f(g(x)) != x for some x. Usually people just need to be able to correctly deserialize any valid serialized string, and preferably detect when a serialized string is invalid. Being able to deserialize some arbitrary string that doesn't represent any valid value but which can somehow still be reserialized into the same arbitrary string is a rather unusual requirement.
thesuperbigfrog 3y ago
"Dafny’s ability to statically check critical properties of your program goes well beyond what mainstream languages can do (that includes you, Rust)." Ada supports Design by Contract preconditions, postconditions, and type invariants that were pioneered by the Eiffel programming language: https://learn.adacore.com/courses/intro-to-ada/chapters/contracts.html https://learn.adacore.com/courses/intro-to-ada/chapters/cont... The SPARK subset of Ada also does static proofs / formal verification: https://learn.adacore.com/courses/intro-to-spark/chapters/01_Overview.html https://learn.adacore.com/courses/intro-to-spark/chapters/01... === Rust has Design by Contract capabilities via the contracts crate: https://docs.rs/contracts/latest/contracts/ https://docs.rs/contracts/latest/contracts/ Maybe one day Rust will have formal verification too? Work is under way: https://alastairreid.github.io/automatic-rust-verification-tools-2021/ https://alastairreid.github.io/automatic-rust-verification-t...
- lionkor 3y ago
  > Rust has Design by Contract capabilities via the contracts crate And C++ has reflection using boost ;)
  - thesuperbigfrog 3y ago
    Contracts for C++ have been proposed: https://www.reddit.com/r/cpp/comments/cmk7ek/what_happened_to_c20_contracts/ https://www.reddit.com/r/cpp/comments/cmk7ek/what_happened_t... Not sure if / when they will land: https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2022/p0592r5.html https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2022/p05...
- jakuj 3y ago
  You might be interested in the Prusti project, which statically checks for absence of reachable panics, overflows etc. It also allows user-defined specifications such as pre and post-conditions, loop body invariants, termination checking and so on. https://github.com/viperproject/prusti-dev https://github.com/viperproject/prusti-dev
- perlgeek 3y ago
looperhacks 3y ago
> The compiler still cannot tell when our loops will terminate (yes, this is possible). Isn't this just the halting problem? Sure, for simple cases compiler could do it (in Java I guess my IDE will do it since the compiler doesn't care), but in the general case, how would a compiler figure this out?
- two_handfuls 3y ago
  Yes, correct. The author is skipping something here. The Dafny compiler only accepts programs if it can prove they terminate. You help it with a “decreases annotation”. So it’s true that no every program provably terminates. But those programs that don’t will be rejected by the Dafny compiler. In practice I suspect this is a good thing overall (writing your loops in such a way that it’s easy to prove they terminate is good style). Official documentation: https://dafny.org/dafny/OnlineTutorial/Termination https://dafny.org/dafny/OnlineTutorial/Termination
- benburton 3y ago
  Thank you. I thought I was going crazy.
- IshKebab 3y ago
  It can't in the general case. When you're writing formally verified code (or hardware design) it is very common for the formal engine to just say "nope! couldn't prove it!". But that doesn't mean it is useless. The halting problem has almost no practical relevance because we don't really care about the general case.
  - redjamjar 3y ago
    > The halting problem has almost no practical relevance because we don't really care about the general case. Yup, agreed
FrustratedMonky 3y ago
Shout out to F#. I think it does a lot of this, doesn't get much respect I think because it is from MS and runs on .NET. Love the type checking, which I think is better than Rusts. But since I think Rust will win the market, I hope it improves.
- lolinder 3y ago
  Dafny also originated in MS and initially targeted .NET. https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/ https://www.microsoft.com/en-us/research/project/dafny-a-lan...
- janAkali 3y ago
  I believe, Nim also has this functionality, although, it uses the [0]Z3Prover tool with a nim frontend [1]DrNim for proving. [0]https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3 [1]https://nim-lang.github.io/Nim/drnim.html https://nim-lang.github.io/Nim/drnim.html
- manaskarekar 3y ago
  > Love the type checking, which I think is better than Rusts. But since I think Rust will win the market, I hope it improves. Could you please elaborate on this? What specific stuff are you suggesting that F# does so well?
  - FrustratedMonky 3y ago
    I'm in-experienced with Rust. So bit subjective. F# uses algebraic types, and compiler can do pretty extensive type checking. I understand Rust also does this, it just seemed like Rust allows some options that make it not as complete. But, I'm not expert on Rust.
scythmic_waves 3y ago
I've not had as much time to look into formal verification as I'd like and this blew me away lemma LemmaFromToBytes(v: nat) ensures FromBytes(ToBytes(v)) == v { // Dafny does all the work! } The compiler can _prove_ one function is the inverse of another? That's so cool. Also I disagree with some of the other posts dismissing the usefulness of this kind of thing. I grant that formally verifying every little piece of my code would be overkill. However, I absolutely want certain core pieces of my application formally verified. I'm gonna have to play with Dafny at some point.
- adjav 3y ago
  You might want to look in Lean 4 at some point too. A lot of work has gone into making it's theorem solving ergonomic and approachable for average programmers.
  - toastal 3y ago
    Why3 ‘extends’ OCaml with similar features as well
  - lenocinor 3y ago
    My personal anecdote is that I tried learning Lean 4 last year with a group of other smart and curious programmers, and after a couple of weeks of trying, we failed to make significant progress learning it and stopped. We had much better luck working with Coq instead.
  - xigoi 3y ago
    I'm trying to learn Lean and like it, but it's terribly lacking documentation.
    - lenocinor 3y ago
      The lacking good docs was what stymied my group too.
- Hardliner66 3y ago
leephillips 3y ago
Very interesting. How would this language, or similar systems, deal with lemmas that are true for real numbers but not always true for floats?
- lolinder 3y ago
  In Dafny's case, they don't: `real` is compiled to a representation like BigRational that actually behaves like a real number. In JavaScript it uses bignumber.js: https://github.com/MikeMcl/bignumber.js https://github.com/MikeMcl/bignumber.js
IshKebab 3y ago
I have tried Dafny. I was quite impressed with how easy it was to set up and the integration with VSCode (even though it was fairly buggy). However it was very difficult to prove things. I often ran into cases where could prove something for 3 byte values, but not 4 bytes, and when I asked about it the answer depended on some really really hardcore internal knowledge of how it worked. E.g. when exactly functions are inlined. So I love the idea, but in practice it seems like it is currently only really usable by people who know how it works internally. That isn't the case with the hardware formal verification tools I've used (e.g. VC Formal) which I have very little clue how they work (it's basically magic as far as anyone I've asked is concerned) but I can use them very easily. I suspect formally verifying hardware is easier than software but there you go.
a1o 3y ago
I think C++ may get something like this with contracts, which hopefully makes in C++23!
tromp 3y ago
An introductory course to the use of Dafny for writing programs with fully verified specifications may be found at [1]. [1] https://www.doc.ic.ac.uk/~scd/Dafny_Material/Lectures.pdf https://www.doc.ic.ac.uk/~scd/Dafny_Material/Lectures.pdf
- sn9 3y ago
  And a whole textbook was recently published as well: https://mitpress.mit.edu/9780262546232/program-proofs/ https://mitpress.mit.edu/9780262546232/program-proofs/
apatil 3y ago
Could anyone comment on how often Dafny finds proofs for useful theorems on its own in practice, without requiring the programmer to use expert knowledge of the proof search system to break it down into a sequence of gettable lemmas and/or refactor the code? If the answer is "not that often", is there a possibility that LLM integration could help with proof search? This seems like an application where getting it 95% right is actually OK since proofs generated by the LLM can be automatically checked for correctness.
- redjamjar 3y ago
  I think LLM can help here in various ways. For example, by inferring preconditions/postconditions and loop invariants automatically. Also, perhaps, by writing lemmas as required automatically. I'd guess there has been some work on this already, but not sure.
eterevsky 3y ago
Formal verification is very cool and definitely has its uses (https://www.sigops.org/s/conferences/sosp/2009/papers/klein-sosp09.pdf https://www.sigops.org/s/conferences/sosp/2009/papers/klein-...). From what I heard at least some chip manufacturers do formal verification of their chip designs. But I don't think it scales to general-purpose programming. Most of the easy-to-verify conditions could (and should) be checked by asserts and unit tests. But there's a whole layer of complexity on top of that and in my experience it accounts for the bigger share of bugs.
- tempodox 3y ago
  That's like saying that motor-driven vehicles are not for common use an that your vehicle could and should be driven by a horse.
  - Linell 3y ago
    How?
  - RGBCube 3y ago
    If it was easier to use, manouver and maintain a horse, your claim would be true.
  - eterevsky 3y ago
    Sorry I wasn't clear. I didn't mean to imply that languages with formal verification are inherently worse than those without it. To the contrary, if a language would have formal verification in addition to all the features and an ecosystem of a modern language, I would gladly use it. My point is that for most use cases formal verification by itself is less important than all the other stuff.
    - tempodox 3y ago
      I understand, and I concur.
fjfaase 3y ago
This is indeed an interesting approach, but I wonder whether it also allows you to define 'implementations'. Let me explain. A lot of software development done is because computers are too slow for our demand.[1] It is nice to have an integer type 'nat' that can hold arbitrary large integer numbers (at least as large as fits in the memory model, I presume), but it is not very efficient to use it for every purpose. You also would like to have methods to verify that a certain implementation of a program using a certain 'limited' representation of integers, is correct. [1] https://www.iwriteiam.nl/AoP.html https://www.iwriteiam.nl/AoP.html
- skydhash 3y ago
  You may want to do a Find and Replace (piramid to pyramid).
- redjamjar 3y ago
  So, you can use fixed-width data types in Dafny and verify properties about functions using them. For example, in our EVM implementation we have types like u8, u16, u256, etc. Of course, Dafny won't let operations on these types underflow or overflow, so it does mean more work ensuring your code doesn't allow this.
ComputerGuru 3y ago
The post missed something very important! The whole time I was reading I was thinking to myself “good luck keeping your code error-free after you’re done transcoding from Dafny to the language you actually use in-prod” but… The language (Dafny): https://github.com/dafny-lang/dafny https://github.com/dafny-lang/dafny Dafny is a verification-ready programming language. As you type in your program, Dafny's verifier constantly looks over your shoulder, flags any errors, shows you counterexamples, and congratulates you when your code matches your specifications. When you're done, Dafny can compile your code to C#, Go, Python, Java, or JavaScript (more to come!), so it can integrate with your existing workflow.
- redjamjar 3y ago
  Yeah, so as I understand it, AWS is using Dafny generated (Java) code in production. I think we can assume it won't be as efficient has hand written code (at this stage anyway) but it does give you the added guarantees.
  - ComputerGuru 3y ago
    > I think we can assume it won't be as efficient has hand written code Actually, surprisingly, not necessarily the case! If you'll refer to the discussion in https://github.com/dafny-lang/dafny/issues/601 https://github.com/dafny-lang/dafny/issues/601 and in https://github.com/dafny-lang/dafny/issues/547 https://github.com/dafny-lang/dafny/issues/547, Dafny can statically prove that certain compiler branches are not possible and will never be taken (such as out-of-bounds on index access, logical assumptions about whether a value is greater than or less than some other value, etc). This lets you code in the assumptions (__assume in C++ or unreachable_unchecked() under rust) in the generated production code that will then allow the compiler to optimize the codegen using this information. (Caveat: I just heard of Dafny today. Definitely not an expert!)
haolez 3y ago
If Dafny is not production ready, what language can I use with similar formal verification features and that is already used in production in mission critical environments?
iasdj38103 3y ago
Amazon uses Dafny to ensure that their authorization engine makes correct decisions: https://www.amazon.science/blog/how-we-built-cedar-with-automated-reasoning-and-differential-testing https://www.amazon.science/blog/how-we-built-cedar-with-auto...
ctsk 3y ago
The GCD code seems underspecified - it only guarantees that the result is a common divisor, but not that it’s the greatest common divisor.
zoogeny 3y ago
I like that things like this exist even if I recognize that they are not for me. For some class of system I am sure these languages will shine. It reminds me of Julia - every time I come across it I love the idea of it but I have no personal use for it. I'm always interested in reading articles on dependent type languages like Coq and Idris but I haven't even tried to write a "Hello, World!" in them. I may just be jaded with promises of sufficiently smart compilers. I actually hold out more hope for AI code assistance than I do for easy-to-use formal verification. It is a bit like Esperanto or something like that. Maybe I am just brain damaged from growing up in a world with English and other messy spoken languages but my intuition suggests that perfectly structured languages are possibly the wrong approach. Even though at the time I wanted xhtml to win the battle of structured formats for the web, in hindsight I now believe messy html 5 was the way to go. > We still get buffer overflows and integer overflows. The compiler still cannot tell when our loops will terminate (yes, this is possible). Aliasing is still a complete unbridled mess. As strange as it sounds, I've learned to love the flaws. I don't see my job in life is to remove every possible source of error. There seems to be a balance point where the cure is worse than the disease and I wish to find that balance point rather than some theoretical perfect. So I do hate those things listed. But so far, the balance point for me is with languages that sacrifice perfectly solving those problems.
- nine_k 3y ago
  Highly regular natural languages exist and thrive. I'd say that Japanese is a way, way more regularly structured language than English. Loving flaws like buffer overflows looks more like a Stockholm syndrome to me: when the reality is terrible, people learn to find lovable bits in it, just to avoid insanity. C has its place, but its place is very, very close to hardware. (And I hope Zig will push it from there, too, eventually.) I don't think that better static guarantees are going to come from direct adoption of languages like Haskell, or some tools like Coq or Agda. They will continue coming the same way Rust and Typescript gone mainstream: by integrating them into practical (not research) languages, and allowing escape hatches, prominently marked. Advanced features need adaptation to be ergonomic, after that they feel natural. This happens to every scientific achievement that has a large practical value: compare a laser on an optical workbench in a lab to a laser in a DVD drive, or a laser pointer. I would likely laugh if someone told me in 1995 that pure FP approaches will conquer GUI development. Nevertheless, this happened twice: first with XSLT in 2000s, then with React in 2010s.
armchairhacker 3y ago
The problem with Dafny and other SMT solvers is that when they work, they're brilliant, but when they don't, they're infuriating. Sometimes your code and theorems are formed in a way which Dafny is very good at reasoning about (e.g. standard induction). Then it's nice to just write code and have everything verify. Other times your assertions are non-trivial to the verifier, even if they look obvious, and you must write lemmas and assertions to get them to be proven. And the problem with SMT solvers is that it can be hard to figure out which lemmas and assertions you need to add. It's frustrating to see some assertion Dafny can't prove, which to you seems almost self-evident, and it can be hard to see what is missing. Languages like Coq, Lean, and Isabelle/HOL are better in that you prove things manually (unless you abuse `auto` and tactics for non-trivial proofs, then you still run into the above). Because when you're writing a manual proof, you know exactly what you have and what you need to prove and why the two aren't yet the same. It can still be frustrating but less so, because in Coq you usually have a better idea what key details are unproven, whereas in Dafny you just get "this (entire statement) can't be proved". You could also say that Coq goes "above and beyond" even though you must write the proofs manually, because you can statically check arbitrary properties and write "safe" code which upholds extremely complex invariants using dependent types. But ultimately, any formal verification language becomes extremely verbose and challenging to write once the properties you are trying to statically prove become mildly complicated. Which is why most code doesn't go "above and beyond" even though formal methods have been around for decades. It's an unfortunate reality in the field: you can spend decades writing a formally-verified version of a medium-sized program, or could spend weeks writing the program itself and then writing solid tests (see: CompCert, sel4). But I still think we're making progress: case in point Rust (and other new languages with ownership semantics), and companies actually using formal methods to verify the small but critical parts of your code.
- redjamjar 3y ago
  > The problem with Dafny and other SMT solvers is that when they work, they're brilliant, but when they don't, they're infuriating Yeah, look I'm not going to disagree with that. I have had plenty of frustrating times figuring out why something won't verify with Dafny. But, the more you do it, the easier it gets. And, we should work on the assumption that these tools will get better. > Languages like Coq, Lean, and Isabelle/HOL are better in that you prove things manually (unless you abuse `auto` and tactics for non-trivial proofs, then you still run into the above). So, it is nice that you always feel like you can make progress with these tools. But, at the same time, that progress can be awfully slow and painstaking. I think the sweet spot lies in using automation as much as possible, but with the fall back option of proving things manually. Dafny to some extent lets you do this, as you can always fall back on manual induction using a lemma.
_a_a_a_ 3y ago
Static typing in programming languages are propositions[1] that the type checker proves (because it is a prover of sorts). It's very simple; it has to be simple to ensure that it's reasonably fast and above all, terminates with a clear yes/no. It's a bit off for this article not to mention that whatever cleverness underlies these examples, things will fail. That is it may not terminate in general, and if it does it might well do so without proving anything useful. I really, really like the idea of formal methods and I would really, really love to use them but they don't come for free unfortunately. [1] in an informal sense, perhaps calling them proposals might be better
contravariant 3y ago
Interestingly the postcondition does not prove that the GCD implementation is correct and by extension does not prove Bézout's identity. Stating that some value is the gcd is surprisingly tricky. Once you have proven that Bézout's identity holds for your function you could prove it is the actual gcd by showing it is a divisor for both a an b. Assuming I understood the notation correctly that would give something like the following lemma euclid_gcd(nat: a, nat: b) ensures (a % GCD(a,b)) == 0 ensures (b % GCD(a,b)) == 0 { } I'd be curious to know if it can prove this. Note that this would still not constitute a proof of Bézout's identity, as it uses it to define what the gcd is. Thankfully defining the gcd using Bézout's identity is pretty common nowadays, as it allows for a useful generalisation of the concept.
- jcparkyn 3y ago
  I think even your example is not actually proving GCD, just that the result is _a_ common divisor. E.g. it would succeed if GCD(a, b) = 1 for all a, b.
  - contravariant 3y ago
    It would, but combined with the postcondition you then get gcd(a,b) = ax + by = 1, which shows the gcd is indeed 1.
galkk 3y ago
lemma LemmaFromToBytes(v: nat) ensures FromBytes(ToBytes(v)) == v { // Dafny does all the work! } > This might not seem like much, but it represents something you cannot easily do in other languages. This lemma asks Dafny to check that, for any possible nat value v, it always holds that FromBytes(ToBytes(v)) == v. Again, Dafny checks this at compile time — no testing required! --- How long does it take, do we rely on caching compilation results here? Is it iterating through all values?
tmtvl 3y ago
Theorem proving is a interesting area of Computer Science. I personally like using ACL2, which has proven itself through industrial use: <https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5597723/ https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5597723/>.
llama123 3y ago
well this is a surprise, He was my old lecture (one of the best at my university tbh). Was always obsessed with formal verification. I remember him trying make us use a formal verification programming language he created called whiley, Which was a java based language and was pretty terrible and filled with bugs lol but had some cool ideas in it
livinginfear 3y ago
Cool article. This language looks really interesting. The only problem though is, how do I use it? The majority of the programming I do in my daily life revolves around performing actions in a database based upon the contents of HTTP requests. There's lots of amazing programming languages out there, however there don't seem to be any really pushing the boundaries for web programming.
deterministic 3y ago
Dafny is an amazing language. A clear step forward when it comes to writing correct code.

338 points by rrampage 3y ago

>function Gcd(a:nat, b:nat) : (g:nat,x:int,y:int)) I hope this is a typo. Otherwise it…requires an unmatched close paren? That's a new level of cursed syntax. EDIT: Also, is |array| a common way to get the length of an array in languages? I've never seen that (or some of this other syntax) before and it took me a minute to figure out what was happening.

jbl 3y ago
|array| looks like it’s taken from the notation for cardinality of a set (number of elements in a set)
- snitty 3y ago
  That makes sense. I initially read it as "absolute value." Which, admittedly, doesn't make sense for an array, but is a reasonable interpretation at first blush.
hdctambien 3y ago
I don't know about programming languages, but in mathematics |v| is the notation to get the length of a vector... So maybe Matlab uses that syntax?
- deleted 3y ago
  [deleted]
- RGBCube 3y ago
  FYI, MATLAB uses `length(v)` to get the length of vector v.
deleted 3y ago
[deleted]
redjamjar 3y ago
> I hope this is a typo Yeah, sorry --- that is a typo.

artemonster 3y ago

I have a very bad opinion about this, why there were no quantum leaps in programming: in practical world there is just no time to think out of the box. its an endless crunch and race to ship, so something brand new and „risky“ can only be born out of strong vision and necessity. On the other hand if we take PL research - it is too far detached from practical reality. Have you ever tried grokking type proofs? It is driven by a separate breed of mathematicians that cosplay as programmers and they build their „perfect and sound“ (and useless) world. Do you know how many tons of (garbage) papers were in the era when AOP was the rage? What are the practical results? And where are they? Or take Haskell as an emple, where nobody can clearly explain to a java codemonkey what a goddamn monad is? Or endless continuations and effects research and formalisms by Felleisen and Kiselyov only for all of it be kinda rediscovered and slapped on by react devs? Useless, all of it.

anonzzzies 3y ago
Everyone can explain to everyone what a monad is for and how to use it. The fundamentals in category theory, you really don't need. But because it got such a bad name, everyone is afraid and believes it must be much harder than they think. Dependent types and other proofs are not that hard to understand in principle; you can be working on them for a very long and that indeed makes it mostly impractical. However, we will see some interesting things in search space limiting between program synthesis, verification and LLMs. I tend to prove only the parts that are vital and the things that come automatic (when the holes are automatically filled because they are already 'done').
- c_crank 3y ago
  Explaining how to use a Javascript Promise is simple. Explaining how to write idiomatic pure code using Monads is hard, and impractical in most cases, despite what FP purists will tell you.
  - anonzzzies 3y ago
    Yes, that's true, but in general programming is not easy, especially when there is something at stake (so probably most professionally written software) and as i'm work as an enterprise troubleshooter mostly in banking/insurance/trading, the depressing amounts of javascript/typescript code I encounter that should never have been put in production, while I hardly ever encounter bad f#, ocaml, rust, haskell or c++ (modern versions). Sometimes it's not excellent, but it's never as bad as the vast majority of nodejs running projects. The programmers of the latter are far more rigid, because it's hard to do anything, but when you do, you get rewarded. People learn JS in 2 days, slap on :any and blam, typescript gurus, get a job, create a system that processes millions$ and then leave for the next 'adventure'. People who invest in rigidity create better software. But yeah, they are far thinner in the 'get shit done fast' arena. So yes, I agree, if you want something done quickly and don't mind if it expires a few months later, you don't grab haskell, rust and definitely not a dependently typed language or proof assistent.

Jeff_Brown 3y ago

I'm a believer too (in dependent types). Software already bears an ungodly amount of responsibility, and with AI it will only become more so. Correctness is critical. While tests are good, it's impossible yo cover every case. Compiler-verifiable properties are better.

wredue 3y ago
[flagged]
- consilient 3y ago
  > who still cannot formally prove a linked list properly after decades. Huh? Prove what about a linked list? https://www.idris-lang.org/docs/idris2/current/base_docs/docs/Data.List.html https://www.idris-lang.org/docs/idris2/current/base_docs/doc... seems like a perfectly good dependently-typed linked list to me.
  - astrange 3y ago
    Which makes it useless, since despite their teaching-programming popularity, linked lists aren't actually good for anything. The useful kind is called intrusive linked lists, but nobody teaches those.
    - consilient 3y ago
      Intrusive linked lists trade away simplicity and ease of refactoring for better memory characteristics. There's a huge amount of code where that trade is a terrible deal. Obviously you shouldn't use ordinary linked lists deep in the guts of an OS kernel or automated trading system but claiming that they're useless is absurd.
      - astrange 3y ago
        The main issue is that a list of pointers is inefficient but also overkill; a small list is probably fine as an array even if you're mutating it. But intrusive lists also have clearer ownership, since the object knows all the lists it can be in, and that's handy sometimes.

anonzzzies 3y ago

Hope people are not going to mention that this is a blockchain company. No matter how I don't like it; this work, research and others (like Wadler) is great and very interesting advancements in the software verification space. You can ignore the blockchain side of things.

john-radio 3y ago
> You can ignore the blockchain side of things. You can, but you don't have to...
simpsond 3y ago
Verification of onchain protocols seems like a great fit.
- anonzzzies 3y ago
  It is, it advances this theory and tech. I only mentioned it because many people will simply not read anything that has blockchain associations.
  - classified 3y ago
    Blockchain is just a solution in search of a problem. It's the cryptocurrency stuff where it gets shady.
hobofan 3y ago
> Hope people are not going to mention that this is a blockchain company. Well, nobody apart from you did...

Arainach 3y ago

SAT solvers are fun. Math is fun. Neither is the most important part of development. Most of my time is not spent formally testing these methods; it is understanding how systems interact and their performance characteristics. I disagree with OP's assertion about legacy languages; they have largely focused their improvements on the areas that actually matter to my day to day development.

anonzzzies 3y ago
> it is understanding how systems interact and their performance characteristics. But there is, at least a theoretical, promise that when you are rigid enough in your types, you are able to predict & prove memory, cpu, network use etc. It's pie in the sky, especially for interacting systems, but there is some future to cling on to. When doing embedded work, I use some of these to make sure algorithms stay within the limits in a way that they won't compile if they don't. There are also provable security which I also use (sparingly). We will get there, hopefully before I give up coding and become a fultime carpenter.
- AnimalMuppet 3y ago
  I think you are on the path that is how this will actually be used: It gets added in little bits. I could be rigid enough with my types to prove more than I do. I don't because the payback isn't worth the effort. When it is worth the effort, then people will (gradually start to) use it. > When doing embedded work, I use some of these to make sure algorithms stay within the limits in a way that they won't compile if they don't. Could you be a bit more specific here about what you do, why you do it in embedded (and not elsewhere), what it protects you from, and how it does so?
  - anonzzzies 3y ago
    > Could you be a bit more specific here about what you do, why you do it in embedded (and not elsewhere), what it protects you from, and how it does so? We create, upgrade, maintain, validate applets for emv and other cryptographic and sensitive embedded (MCUs) applications; I try to guarantee safety using tla+, coq, z3 and agda. Or just on paper. And we deliver that as paper with our software. It’s just some functions, not all: we often have to, because of certification, show ‘a story’ (not proof) that things will be ‘secure enough’. I personally enjoy it more to prove some of the crucial parts as ‘the story’ not write a story.

agentultra 3y ago

Dafny is a cool language. Conal Eliot, in his 2023 Zurihac talk, says that in order to get efficiency (faster computers that can do more with less) at scale (not merely resilience which we get by adding redundancy and operational tooling) we need languages and tools that allow us to precisely specify the correct program. Dafny is a good step in that direction. I’m also keen to see where the depedently typed programming languages like Lean 4 and Idris 2 will take us. Proof-carrying code could be very useful.

practal 3y ago
Thanks for pointing out the Conal Elliott talk. Just watched it, very nice talk. I found myself nodding to pretty much everything he said, except of his fondness for dependent types. Each time he says "dependent types", I just replace it in my mind with "logic". I think he will transition eventually: Types (Haskell) -> Dependent Types (Agda) -> Logic (Practal), hehehe.
- agentultra 3y ago
  Well you can encode any logic you want in dependent types, so yeah probably!
  - practal 3y ago
    Fair enough. Although to encode a proposition as a type, only to then view it as a proposition again, would be two wrappers too many for my taste. I prefer to keep the notions of truth and types apart. In practice, this makes the logic both simpler and more expressive.
sn9 3y ago
Talk link: https://youtu.be/k6rY5Mvx84E https://youtu.be/k6rY5Mvx84E

TrueDuality 3y ago

This is pretty cool! I do have a nitpick I think is important. An empty byte array getting converted to zero seems like a bad edge case that should probably produce some kind of error invariant. This isn't a minor concern if the intent is to use this in serious applications that require this degree of formalism. The two proofs are easy to break: `ToBytes(FromBytes([])) != []`. It's an obvious example of the issue: FromBytes handles inputs ToBytes can't generate therefore they are not true inverses of each other. It's a simple case but it was quick to find in this simple example, and it hints at dangerous oversights that could lead to severe bugs in more complex scenarios, like in cryptography. It's critical to account for such edge cases.

occamrazor 3y ago
TFA makes exactly this point. The lemma that Dafny proves is true, the reversed one is not and Dafny can provide the counterexample (the empty list).
- TrueDuality 3y ago
  I didn't notice that it is kind of called out in the post... It's the very last line and left as an exercise to the reader to infer which is almost worse since I would call this a flaw in the implementation of the functions and is being shown off as a sterling example of the capabilities of the language. The conversion between `[]` and `0` is the flaw that is hard to reason about here and propagates through any code that interacts with it in a way that violates a programmers expectations.
  - fluoridation 3y ago
    It's not that uncommon to have de/serialization functions where g(f(x)) == x for all x, but f(g(x)) != x for some x. Usually people just need to be able to correctly deserialize any valid serialized string, and preferably detect when a serialized string is invalid. Being able to deserialize some arbitrary string that doesn't represent any valid value but which can somehow still be reserialized into the same arbitrary string is a rather unusual requirement.

thesuperbigfrog 3y ago

"Dafny’s ability to statically check critical properties of your program goes well beyond what mainstream languages can do (that includes you, Rust)." Ada supports Design by Contract preconditions, postconditions, and type invariants that were pioneered by the Eiffel programming language: https://learn.adacore.com/courses/intro-to-ada/chapters/contracts.html https://learn.adacore.com/courses/intro-to-ada/chapters/cont... The SPARK subset of Ada also does static proofs / formal verification: https://learn.adacore.com/courses/intro-to-spark/chapters/01_Overview.html https://learn.adacore.com/courses/intro-to-spark/chapters/01... === Rust has Design by Contract capabilities via the contracts crate: https://docs.rs/contracts/latest/contracts/ https://docs.rs/contracts/latest/contracts/ Maybe one day Rust will have formal verification too? Work is under way: https://alastairreid.github.io/automatic-rust-verification-tools-2021/ https://alastairreid.github.io/automatic-rust-verification-t...

lionkor 3y ago
> Rust has Design by Contract capabilities via the contracts crate And C++ has reflection using boost ;)
- thesuperbigfrog 3y ago
  Contracts for C++ have been proposed: https://www.reddit.com/r/cpp/comments/cmk7ek/what_happened_to_c20_contracts/ https://www.reddit.com/r/cpp/comments/cmk7ek/what_happened_t... Not sure if / when they will land: https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2022/p0592r5.html https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2022/p05...
jakuj 3y ago
You might be interested in the Prusti project, which statically checks for absence of reachable panics, overflows etc. It also allows user-defined specifications such as pre and post-conditions, loop body invariants, termination checking and so on. https://github.com/viperproject/prusti-dev https://github.com/viperproject/prusti-dev
perlgeek 3y ago

looperhacks 3y ago

> The compiler still cannot tell when our loops will terminate (yes, this is possible). Isn't this just the halting problem? Sure, for simple cases compiler could do it (in Java I guess my IDE will do it since the compiler doesn't care), but in the general case, how would a compiler figure this out?

two_handfuls 3y ago
Yes, correct. The author is skipping something here. The Dafny compiler only accepts programs if it can prove they terminate. You help it with a “decreases annotation”. So it’s true that no every program provably terminates. But those programs that don’t will be rejected by the Dafny compiler. In practice I suspect this is a good thing overall (writing your loops in such a way that it’s easy to prove they terminate is good style). Official documentation: https://dafny.org/dafny/OnlineTutorial/Termination https://dafny.org/dafny/OnlineTutorial/Termination
benburton 3y ago
Thank you. I thought I was going crazy.
IshKebab 3y ago
It can't in the general case. When you're writing formally verified code (or hardware design) it is very common for the formal engine to just say "nope! couldn't prove it!". But that doesn't mean it is useless. The halting problem has almost no practical relevance because we don't really care about the general case.
- redjamjar 3y ago
  > The halting problem has almost no practical relevance because we don't really care about the general case. Yup, agreed

FrustratedMonky 3y ago

Shout out to F#. I think it does a lot of this, doesn't get much respect I think because it is from MS and runs on .NET. Love the type checking, which I think is better than Rusts. But since I think Rust will win the market, I hope it improves.

lolinder 3y ago
Dafny also originated in MS and initially targeted .NET. https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/ https://www.microsoft.com/en-us/research/project/dafny-a-lan...
janAkali 3y ago
I believe, Nim also has this functionality, although, it uses the [0]Z3Prover tool with a nim frontend [1]DrNim for proving. [0]https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3 [1]https://nim-lang.github.io/Nim/drnim.html https://nim-lang.github.io/Nim/drnim.html
manaskarekar 3y ago
> Love the type checking, which I think is better than Rusts. But since I think Rust will win the market, I hope it improves. Could you please elaborate on this? What specific stuff are you suggesting that F# does so well?
- FrustratedMonky 3y ago
  I'm in-experienced with Rust. So bit subjective. F# uses algebraic types, and compiler can do pretty extensive type checking. I understand Rust also does this, it just seemed like Rust allows some options that make it not as complete. But, I'm not expert on Rust.

scythmic_waves 3y ago

I've not had as much time to look into formal verification as I'd like and this blew me away lemma LemmaFromToBytes(v: nat) ensures FromBytes(ToBytes(v)) == v { // Dafny does all the work! } The compiler can _prove_ one function is the inverse of another? That's so cool. Also I disagree with some of the other posts dismissing the usefulness of this kind of thing. I grant that formally verifying every little piece of my code would be overkill. However, I absolutely want certain core pieces of my application formally verified. I'm gonna have to play with Dafny at some point.

adjav 3y ago
You might want to look in Lean 4 at some point too. A lot of work has gone into making it's theorem solving ergonomic and approachable for average programmers.
- toastal 3y ago
  Why3 ‘extends’ OCaml with similar features as well
- lenocinor 3y ago
  My personal anecdote is that I tried learning Lean 4 last year with a group of other smart and curious programmers, and after a couple of weeks of trying, we failed to make significant progress learning it and stopped. We had much better luck working with Coq instead.
- xigoi 3y ago
  I'm trying to learn Lean and like it, but it's terribly lacking documentation.
  - lenocinor 3y ago
    The lacking good docs was what stymied my group too.
Hardliner66 3y ago

leephillips 3y ago

Very interesting. How would this language, or similar systems, deal with lemmas that are true for real numbers but not always true for floats?

lolinder 3y ago
In Dafny's case, they don't: `real` is compiled to a representation like BigRational that actually behaves like a real number. In JavaScript it uses bignumber.js: https://github.com/MikeMcl/bignumber.js https://github.com/MikeMcl/bignumber.js

IshKebab 3y ago

I have tried Dafny. I was quite impressed with how easy it was to set up and the integration with VSCode (even though it was fairly buggy). However it was very difficult to prove things. I often ran into cases where could prove something for 3 byte values, but not 4 bytes, and when I asked about it the answer depended on some really really hardcore internal knowledge of how it worked. E.g. when exactly functions are inlined. So I love the idea, but in practice it seems like it is currently only really usable by people who know how it works internally. That isn't the case with the hardware formal verification tools I've used (e.g. VC Formal) which I have very little clue how they work (it's basically magic as far as anyone I've asked is concerned) but I can use them very easily. I suspect formally verifying hardware is easier than software but there you go.

a1o 3y ago

I think C++ may get something like this with contracts, which hopefully makes in C++23!

tromp 3y ago

An introductory course to the use of Dafny for writing programs with fully verified specifications may be found at [1]. [1] https://www.doc.ic.ac.uk/~scd/Dafny_Material/Lectures.pdf https://www.doc.ic.ac.uk/~scd/Dafny_Material/Lectures.pdf

sn9 3y ago
And a whole textbook was recently published as well: https://mitpress.mit.edu/9780262546232/program-proofs/ https://mitpress.mit.edu/9780262546232/program-proofs/

apatil 3y ago

Could anyone comment on how often Dafny finds proofs for useful theorems on its own in practice, without requiring the programmer to use expert knowledge of the proof search system to break it down into a sequence of gettable lemmas and/or refactor the code? If the answer is "not that often", is there a possibility that LLM integration could help with proof search? This seems like an application where getting it 95% right is actually OK since proofs generated by the LLM can be automatically checked for correctness.

redjamjar 3y ago
I think LLM can help here in various ways. For example, by inferring preconditions/postconditions and loop invariants automatically. Also, perhaps, by writing lemmas as required automatically. I'd guess there has been some work on this already, but not sure.

eterevsky 3y ago

Formal verification is very cool and definitely has its uses (https://www.sigops.org/s/conferences/sosp/2009/papers/klein-sosp09.pdf https://www.sigops.org/s/conferences/sosp/2009/papers/klein-...). From what I heard at least some chip manufacturers do formal verification of their chip designs. But I don't think it scales to general-purpose programming. Most of the easy-to-verify conditions could (and should) be checked by asserts and unit tests. But there's a whole layer of complexity on top of that and in my experience it accounts for the bigger share of bugs.

tempodox 3y ago
That's like saying that motor-driven vehicles are not for common use an that your vehicle could and should be driven by a horse.
- Linell 3y ago
  How?
- RGBCube 3y ago
  If it was easier to use, manouver and maintain a horse, your claim would be true.
- eterevsky 3y ago
  Sorry I wasn't clear. I didn't mean to imply that languages with formal verification are inherently worse than those without it. To the contrary, if a language would have formal verification in addition to all the features and an ecosystem of a modern language, I would gladly use it. My point is that for most use cases formal verification by itself is less important than all the other stuff.
  - tempodox 3y ago
    I understand, and I concur.

fjfaase 3y ago

This is indeed an interesting approach, but I wonder whether it also allows you to define 'implementations'. Let me explain. A lot of software development done is because computers are too slow for our demand.[1] It is nice to have an integer type 'nat' that can hold arbitrary large integer numbers (at least as large as fits in the memory model, I presume), but it is not very efficient to use it for every purpose. You also would like to have methods to verify that a certain implementation of a program using a certain 'limited' representation of integers, is correct. [1] https://www.iwriteiam.nl/AoP.html https://www.iwriteiam.nl/AoP.html

skydhash 3y ago
You may want to do a Find and Replace (piramid to pyramid).
redjamjar 3y ago
So, you can use fixed-width data types in Dafny and verify properties about functions using them. For example, in our EVM implementation we have types like u8, u16, u256, etc. Of course, Dafny won't let operations on these types underflow or overflow, so it does mean more work ensuring your code doesn't allow this.

ComputerGuru 3y ago

The post missed something very important! The whole time I was reading I was thinking to myself “good luck keeping your code error-free after you’re done transcoding from Dafny to the language you actually use in-prod” but… The language (Dafny): https://github.com/dafny-lang/dafny https://github.com/dafny-lang/dafny Dafny is a verification-ready programming language. As you type in your program, Dafny's verifier constantly looks over your shoulder, flags any errors, shows you counterexamples, and congratulates you when your code matches your specifications. When you're done, Dafny can compile your code to C#, Go, Python, Java, or JavaScript (more to come!), so it can integrate with your existing workflow.

redjamjar 3y ago
Yeah, so as I understand it, AWS is using Dafny generated (Java) code in production. I think we can assume it won't be as efficient has hand written code (at this stage anyway) but it does give you the added guarantees.
- ComputerGuru 3y ago
  > I think we can assume it won't be as efficient has hand written code Actually, surprisingly, not necessarily the case! If you'll refer to the discussion in https://github.com/dafny-lang/dafny/issues/601 https://github.com/dafny-lang/dafny/issues/601 and in https://github.com/dafny-lang/dafny/issues/547 https://github.com/dafny-lang/dafny/issues/547, Dafny can statically prove that certain compiler branches are not possible and will never be taken (such as out-of-bounds on index access, logical assumptions about whether a value is greater than or less than some other value, etc). This lets you code in the assumptions (__assume in C++ or unreachable_unchecked() under rust) in the generated production code that will then allow the compiler to optimize the codegen using this information. (Caveat: I just heard of Dafny today. Definitely not an expert!)

haolez 3y ago

If Dafny is not production ready, what language can I use with similar formal verification features and that is already used in production in mission critical environments?

iasdj38103 3y ago

Amazon uses Dafny to ensure that their authorization engine makes correct decisions: https://www.amazon.science/blog/how-we-built-cedar-with-automated-reasoning-and-differential-testing https://www.amazon.science/blog/how-we-built-cedar-with-auto...

ctsk 3y ago

The GCD code seems underspecified - it only guarantees that the result is a common divisor, but not that it’s the greatest common divisor.

zoogeny 3y ago

I like that things like this exist even if I recognize that they are not for me. For some class of system I am sure these languages will shine. It reminds me of Julia - every time I come across it I love the idea of it but I have no personal use for it. I'm always interested in reading articles on dependent type languages like Coq and Idris but I haven't even tried to write a "Hello, World!" in them. I may just be jaded with promises of sufficiently smart compilers. I actually hold out more hope for AI code assistance than I do for easy-to-use formal verification. It is a bit like Esperanto or something like that. Maybe I am just brain damaged from growing up in a world with English and other messy spoken languages but my intuition suggests that perfectly structured languages are possibly the wrong approach. Even though at the time I wanted xhtml to win the battle of structured formats for the web, in hindsight I now believe messy html 5 was the way to go. > We still get buffer overflows and integer overflows. The compiler still cannot tell when our loops will terminate (yes, this is possible). Aliasing is still a complete unbridled mess. As strange as it sounds, I've learned to love the flaws. I don't see my job in life is to remove every possible source of error. There seems to be a balance point where the cure is worse than the disease and I wish to find that balance point rather than some theoretical perfect. So I do hate those things listed. But so far, the balance point for me is with languages that sacrifice perfectly solving those problems.

nine_k 3y ago
Highly regular natural languages exist and thrive. I'd say that Japanese is a way, way more regularly structured language than English. Loving flaws like buffer overflows looks more like a Stockholm syndrome to me: when the reality is terrible, people learn to find lovable bits in it, just to avoid insanity. C has its place, but its place is very, very close to hardware. (And I hope Zig will push it from there, too, eventually.) I don't think that better static guarantees are going to come from direct adoption of languages like Haskell, or some tools like Coq or Agda. They will continue coming the same way Rust and Typescript gone mainstream: by integrating them into practical (not research) languages, and allowing escape hatches, prominently marked. Advanced features need adaptation to be ergonomic, after that they feel natural. This happens to every scientific achievement that has a large practical value: compare a laser on an optical workbench in a lab to a laser in a DVD drive, or a laser pointer. I would likely laugh if someone told me in 1995 that pure FP approaches will conquer GUI development. Nevertheless, this happened twice: first with XSLT in 2000s, then with React in 2010s.

armchairhacker 3y ago

The problem with Dafny and other SMT solvers is that when they work, they're brilliant, but when they don't, they're infuriating. Sometimes your code and theorems are formed in a way which Dafny is very good at reasoning about (e.g. standard induction). Then it's nice to just write code and have everything verify. Other times your assertions are non-trivial to the verifier, even if they look obvious, and you must write lemmas and assertions to get them to be proven. And the problem with SMT solvers is that it can be hard to figure out which lemmas and assertions you need to add. It's frustrating to see some assertion Dafny can't prove, which to you seems almost self-evident, and it can be hard to see what is missing. Languages like Coq, Lean, and Isabelle/HOL are better in that you prove things manually (unless you abuse `auto` and tactics for non-trivial proofs, then you still run into the above). Because when you're writing a manual proof, you know exactly what you have and what you need to prove and why the two aren't yet the same. It can still be frustrating but less so, because in Coq you usually have a better idea what key details are unproven, whereas in Dafny you just get "this (entire statement) can't be proved". You could also say that Coq goes "above and beyond" even though you must write the proofs manually, because you can statically check arbitrary properties and write "safe" code which upholds extremely complex invariants using dependent types. But ultimately, any formal verification language becomes extremely verbose and challenging to write once the properties you are trying to statically prove become mildly complicated. Which is why most code doesn't go "above and beyond" even though formal methods have been around for decades. It's an unfortunate reality in the field: you can spend decades writing a formally-verified version of a medium-sized program, or could spend weeks writing the program itself and then writing solid tests (see: CompCert, sel4). But I still think we're making progress: case in point Rust (and other new languages with ownership semantics), and companies actually using formal methods to verify the small but critical parts of your code.

redjamjar 3y ago
> The problem with Dafny and other SMT solvers is that when they work, they're brilliant, but when they don't, they're infuriating Yeah, look I'm not going to disagree with that. I have had plenty of frustrating times figuring out why something won't verify with Dafny. But, the more you do it, the easier it gets. And, we should work on the assumption that these tools will get better. > Languages like Coq, Lean, and Isabelle/HOL are better in that you prove things manually (unless you abuse `auto` and tactics for non-trivial proofs, then you still run into the above). So, it is nice that you always feel like you can make progress with these tools. But, at the same time, that progress can be awfully slow and painstaking. I think the sweet spot lies in using automation as much as possible, but with the fall back option of proving things manually. Dafny to some extent lets you do this, as you can always fall back on manual induction using a lemma.

_a_a_a_ 3y ago

Static typing in programming languages are propositions[1] that the type checker proves (because it is a prover of sorts). It's very simple; it has to be simple to ensure that it's reasonably fast and above all, terminates with a clear yes/no. It's a bit off for this article not to mention that whatever cleverness underlies these examples, things will fail. That is it may not terminate in general, and if it does it might well do so without proving anything useful. I really, really like the idea of formal methods and I would really, really love to use them but they don't come for free unfortunately. [1] in an informal sense, perhaps calling them proposals might be better

contravariant 3y ago

Interestingly the postcondition does not prove that the GCD implementation is correct and by extension does not prove Bézout's identity. Stating that some value is the gcd is surprisingly tricky. Once you have proven that Bézout's identity holds for your function you could prove it is the actual gcd by showing it is a divisor for both a an b. Assuming I understood the notation correctly that would give something like the following lemma euclid_gcd(nat: a, nat: b) ensures (a % GCD(a,b)) == 0 ensures (b % GCD(a,b)) == 0 { } I'd be curious to know if it can prove this. Note that this would still not constitute a proof of Bézout's identity, as it uses it to define what the gcd is. Thankfully defining the gcd using Bézout's identity is pretty common nowadays, as it allows for a useful generalisation of the concept.

jcparkyn 3y ago
I think even your example is not actually proving GCD, just that the result is _a_ common divisor. E.g. it would succeed if GCD(a, b) = 1 for all a, b.
- contravariant 3y ago
  It would, but combined with the postcondition you then get gcd(a,b) = ax + by = 1, which shows the gcd is indeed 1.

galkk 3y ago

lemma LemmaFromToBytes(v: nat) ensures FromBytes(ToBytes(v)) == v { // Dafny does all the work! } > This might not seem like much, but it represents something you cannot easily do in other languages. This lemma asks Dafny to check that, for any possible nat value v, it always holds that FromBytes(ToBytes(v)) == v. Again, Dafny checks this at compile time — no testing required! --- How long does it take, do we rely on caching compilation results here? Is it iterating through all values?

tmtvl 3y ago

Theorem proving is a interesting area of Computer Science. I personally like using ACL2, which has proven itself through industrial use: <https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5597723/ https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5597723/>.

llama123 3y ago

well this is a surprise, He was my old lecture (one of the best at my university tbh). Was always obsessed with formal verification. I remember him trying make us use a formal verification programming language he created called whiley, Which was a java based language and was pretty terrible and filled with bugs lol but had some cool ideas in it

livinginfear 3y ago

Cool article. This language looks really interesting. The only problem though is, how do I use it? The majority of the programming I do in my daily life revolves around performing actions in a database based upon the contents of HTTP requests. There's lots of amazing programming languages out there, however there don't seem to be any really pushing the boundaries for web programming.

deterministic 3y ago

Dafny is an amazing language. A clear step forward when it comes to writing correct code.