dafny-lang/dafny on Hacker News

…-- From https://news.ycombinator.com/item?id=28494885#28513982 : > https://github.com/dafny-lang/dafny #read-more > Dafny Cheat Sheet: https://docs.google.com/document/d/1kz5_yqzhrEyXII96eCF1YoHZ... > Looks like there's a Has

comment by westurner · 2024-07-05 · in The sad state of property-based testing libraries

…similar project, Dafny is a "verification-aware programming language" that can compile to rust: https://github.com/dafny-lang/dafny

comment by ComputerGuru · 2024-05-04 · in Verified Rust for low-level systems code

…[2] https://github.com/Z3Prover/z3 [3] https://github.com/microsoft/CodeContracts [4] https://github.com/dafny-lang/dafny [5] https://github.com/dotnet/csharplang/issues/105

comment by Genbox · 2023-10-27 · in Lean4 helped Terence Tao discover a small bug in his recent paper

…It would still be a serious effort of course. [1] https://blog.regehr.org/archives/232 [2] https://github.com/dafny-lang/dafny/blob/master/Test/dafny4/...

comment by User23 · 2023-08-11 · in Fastest branchless binary search

…written code Actually, surprisingly, not necessarily the case! If you'll refer to the discussion in https://github.com/dafny-lang/dafny/issues/601 and in https://github.com/dafny-lang/dafny/issues/547 , Dafny can statically prove that…

comment by ComputerGuru · 2023-06-29 · in Programming languages going above and beyond

…done transcoding from Dafny to the language you actually use in-prod” but… The language (Dafny): https://github.com/dafny-lang/dafny Dafny is a verification-ready programming language. As you type in your program, Dafny's verifier…

comment by ComputerGuru · 2023-06-29 · in Programming languages going above and beyond

…for the sake of change and featuritis are pretty incompatible with it. [1] https://fbinfer.com [2] https://github.com/dafny-lang/dafny

comment by nextos · 2022-08-18 · in Programming breakthroughs we need

…better semantics would be able to offer a lot more guarantees. [1] http://objective.st/About [2] https://github.com/dafny-lang/dafny [3] https://fbinfer.com

comment by nextos · 2022-08-13 · in Objective-S: architecture-oriented language based on Smalltalk and Objective-C

…of them. -------------- [1] https://aws.amazon.com/blogs/security/protect-sensitive-data... [2] https://github.com/dafny-lang/dafny

comment by picardo · 2022-08-08 · in Automated Reasoning at Amazon: A Conversation

Ada is already mentioned here. You also want to look at Dafny for a contract-based language: https://github.com/dafny-lang/dafny Since it has verification support it also covers the second point about semantic relations.

comment by mazesc · 2022-07-13 · in Six programming languages I’d like to see

…can prove useful programs. Apparently, part of the Ethereum 2 specification was verified using it. https://github.com/dafny-lang/dafny I have been learning it and the syntax is close to most C style programming languages. As a software…

comment by hath995 · 2022-05-29 · in Make formal verification and provably correct software practical and mainstream

…are several projects on formal analysis of C. [3][4][5][6] [0] https://github.com/zetzit/zz [1] https://github.com/dafny-lang/dafny [2] https://dafny-lang.github.io/dafny/ [3] https://frama-c.com/ [4] https://www.microsoft.com/en-us/researc…

comment by MaxBarraclough · 2022-01-23 · in ISO C became unusable for operating systems development

…much easier [0][1] and of course there's SPARK Ada. [0] https://github.com/zetzit/zz [1] https://github.com/dafny-lang/dafny

comment by MaxBarraclough · 2021-11-21 · in Foundations of Dawn: The Untyped Concatenative Calculus

https://github.com/dafny-lang/dafny Dafny Cheat Sheet: https://docs.google.com/document/d/1kz5_yqzhrEyXII96eCF1YoHZ... Looks like there's a Haskell-to-Dafny converter.

comment by westurner · 2021-09-13 · in How We Proved the Eth2 Deposit Contract Is Free of Runtime Errors

…//www.microsoft.com/en-us/research/project/vcc-a-verif... [3]: https://github.com/koka-lang/koka [4]: https://github.com/dafny-lang/dafny [5]: https://www.microsoft.com/en-us/research/project/project-ver...

comment by erk__ · 2021-07-06 · in Linux Rust Support

…the lesser-known ZZ and Dafny languages, which look very interesting. https://github.com/aep/zz https://github.com/dafny-lang/dafny

comment by MaxBarraclough · 2021-02-17 · in Inline and Sideline Approaches for Low-Cost Memory Safety in C

…attempts to do something like this for imperative-style languages, using pre- and post-conditions: https://github.com/dafny-lang/dafny

comment by lolinder · 2020-09-18 · in How Did Software Get So Reliable Without Proof? (1996) [pdf]

…which mentioned Microsoft's Dafny language, which includes a program verifier. https://github.com/dafny-lang/dafny Dafny is not on the list of notable programming languages.

comment by eesmith · 2020-02-07 · in There are around ~700 programming languages in the world

…like Dafny[3]. [1] https://github.com/microsoft/vcc [2] http://moskal.me/pdf/tphol2009.pdf [3] https://github.com/dafny-lang/dafny

comment by ausimian · 2020-02-03 · in Jonathan Blow on Rust

a fun exercise is to write this in Dafny https://github.com/dafny-lang/dafny It's simple enough to be attempted with a limited knowledge of Dafny, but subtle enough that you will need to think about what you are doing…

comment by manu3000 · 2019-11-01 · in On Binary Search

…+ web interface at: https://rise4fun.com/Dafny/tutorial/Guide . The official repository is here: https://github.com/Microsoft/dafny -- you might want to switch to a local installation once the online tutorial whets your appetite. A good…

comment by wsxcde · 2019-04-03 · in Loop invariants can give you coding superpowers

…list of "cool things also happen to employ Z3", definitely check out MS Dafny programming language: https://github.com/Microsoft/dafny

comment by Profan · 2019-02-06 · in Programming the Z3 SMT solver

In addition to Dafny ( https://github.com/Microsoft/dafny ) and Whiley ( http://whiley.org/ ), check out Frama-C ( https://frama-c.com/ ) for C and SPARK ( http://www.spark-2014.org/ ) for Ada. Both are mature enough to be in use, but are…

comment by mcguire · 2018-06-08 · in Notes on Idris (2017)

…can use it routinely in mainstream programming is an unsolved problem in December 2017. [1] https://github.com/Microsoft/dafny

comment by YorkshireSeason · 2017-12-15 · in Fourteen Years of Software Engineering at ETH Zurich

…compiles it into a CLR-compatible binary, hence you'll see equivalent C code for comparison) [1] https://github.com/Microsoft/dafny [2] https://github.com/shawa/formal-verification-project

comment by shawa_a_a · 2017-12-11 · in Finding bugs in Haskell code by proving it

…Haskell. " So I'm mostly as happy as a pig in a blanket. (Specifically, take a look at Dafny ( https://github.com/Microsoft/dafny ) (probably the poster child for the verification approach) and Idris ( https://www.idris-lang.org/ ) (voted…

comment by mcguire · 2017-08-19 · in “What next?”

…what I could gather, F* appears to be slightly more general/sophisticated in what it can prove. [1] https://github.com/Microsoft/dafny [2] https://www.fstar-lang.org [3] https://project-everest.github.io [4] https://mitls.org

comment by wizeman · 2016-11-04 · in Rules for Writing Safety Critical Code (2006)