[HN Gopher] Programming languages going above and beyond
___________________________________________________________________
Programming languages going above and beyond
Author : rrampage
Score : 282 points
Date : 2023-06-29 12:29 UTC (10 hours ago)
(HTM) web link (whileydave.com)
(TXT) w3m dump (whileydave.com)
| snitty wrote:
| >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 wrote:
| |array| looks like it's taken from the notation for cardinality
| of a set (number of elements in a set)
| snitty wrote:
| 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.
| [deleted]
| hdctambien wrote:
| 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?
| RGBCube wrote:
| FYI, MATLAB uses `length(v)` to get the length of vector v.
| [deleted]
| redjamjar wrote:
| > I hope this is a typo
|
| Yeah, sorry --- that is a typo.
| _a_a_a_ wrote:
| 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
| leephillips wrote:
| 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 wrote:
| 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
| artemonster wrote:
| 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 wrote:
| 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 wrote:
| 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.
| vore wrote:
| I really don't like how monads get couched in this way:
| they're a fundamental concept that you can see everywhere
| (at least understood by functional programmers with
| Promise.then/Promise.resolve, Array.flatMap/[x], etc.).
| Railing on how "using Monads is hard" makes no sense
| because it's a bit like talking about how using, say,
| Abelian groups are hard when, surprise, you use them every
| day.
| anonzzzies wrote:
| 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.
| FrustratedMonky wrote:
| Have to concur. SO many people grab Python or Javascript
| for a 'quick short script' and it turns into a real
| production system and then becomes un-maintainable. But
| F#, functional languages, they maybe take more time to
| learn, or become proficient, but the errors drop way
| down, because the langue doesn't allow those types of
| errors that are common in 'scripting' languages.
| [deleted]
| c_crank wrote:
| Looks like my previous comment was too mean towards
| JavaScript, so trying this again...
|
| Just using some form of static typing offers easy
| guarantees without much effort. Trying to Monad-ify
| everything for a much smaller level of compiler
| guarantees involves much higher dev effort (as most devs
| do not understand Monads), and much higher effort
| involved in anyone reading the code.
| anonzzzies wrote:
| I agree with this, but I still think it has benefit, if
| only giving a lot of skill to the dev pulling it off.
| It's a trade off of course. I myself like writing and
| reading it more, and I detest 'move fast, break many
| subtle things you will find out only after it's too
| late'. I carved out niches for myself that are hard but
| fulfilling and I don't really need to worry about
| spending months on something some 'gunslinger' can put
| together in 3 days as my clients like long term
| robustness. There are devices out there 2-10 years and
| replacement is painful, so let's not. We see cases with
| clients (I wish I could name: you will know some of them)
| were they have a server in the cloud and client in
| embedded hardware and needing to replace all devices
| because either client or server or both popped a security
| issue that would mess certification.
|
| It is also expensive to fix things without hardware:
| everything is iso/pci and needing recertification to
| changing anything. So the 100k you spend for going for
| perfection pays off. So far at least.
| c_crank wrote:
| What I would take issue with is describing a non
| functional or non Monadified code as something written by
| a gunslinger without care for robustness, as if writing
| things in Monads has a guarantee of robustness or
| correctness or even maintainability.
| anonzzzies wrote:
| My time to peddle back; you are right. Didn't mean to
| imply that, but did.
|
| I do see (irl) that it improves the odds though.
| c_crank wrote:
| My IRL experience with pure functional code in academia
| was so unpleasant that I have since strived to stay as
| far away from it as I possibly can.
| anonzzzies wrote:
| I am not sure we need to go pure functional all over, but
| I recognise your suffering. I mean; I like the
| intellectual challenge of building something 'perfect'
| that cannot be used, however there is a mix to be had. I
| thought Mercury always had a nice idea; its prolog with
| types and adding det makes it stricter.
| jimbob45 wrote:
| Couldn't agree more. I wish we could replace the moniker
| "functional programming" with "aesthetic programming"
| because it feels like Monads are less practical than they
| are hygienic for the code.
| kibwen wrote:
| Using Rust as an example, both the borrow checker ("region-
| based memory management":
| https://www.cs.umd.edu/projects/cyclone/papers/cyclone-regio...
| ) and affine types were "useless" in that they failed to find
| any practical adoption in industry... until they suddenly
| weren't. Nearly the entire field of mathematics is "useless" in
| this way, until one day somebody accidentally invents Boolean
| algebra or Fourier transforms or etc. and changes the world in
| the process.
| contravariant wrote:
| Interestingly the postcondition does not prove that the GCD
| implementation is correct and by extension does not prove
| Bezout's identity.
|
| Stating that some value is the gcd is surprisingly tricky. Once
| you have proven that Bezout'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 Bezout's identity, as it uses it
| to define what the gcd is. Thankfully defining the gcd using
| Bezout's identity is pretty common nowadays, as it allows for a
| useful generalisation of the concept.
| ctsk wrote:
| The GCD code seems underspecified - it only guarantees that the
| result is a common divisor, but not that it's the _greatest_
| common divisor.
| Jeff_Brown wrote:
| 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 wrote:
| Then you're wrong.
|
| Too many people will justify their garbage slow code with an
| immediately unjustifiable statement of "developer time" and
| then turn around and talk about dependant types, who still
| cannot formally prove a linked list properly after decades.
|
| The academics of this are fine, but it'll never reach
| mainstream. Nobody cares, and rightfully so.
| consilient wrote:
| > 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/doc... seems like a
| perfectly good dependently-typed linked list to me.
| anonzzzies wrote:
| 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 wrote:
| > You can ignore the blockchain side of things.
|
| You can, but you don't have to...
| hobofan wrote:
| > Hope people are not going to mention that this is a
| blockchain company.
|
| Well, nobody apart from you did...
| simpsond wrote:
| Verification of onchain protocols seems like a great fit.
| anonzzzies wrote:
| 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 wrote:
| Blockchain is just a solution in search of a problem. It's
| the cryptocurrency stuff where it gets shady.
| IshKebab wrote:
| 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.
| eterevsky wrote:
| Formal verification is very cool and definitely has its uses (htt
| ps://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 wrote:
| 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.
| RGBCube wrote:
| If it was easier to use, manouver and maintain a horse, your
| claim would be true.
| Linell wrote:
| How?
| eterevsky wrote:
| 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.
| armchairhacker wrote:
| 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 wrote:
| > 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.
| haolez wrote:
| 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?
| TrueDuality wrote:
| 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 wrote:
| 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 wrote:
| 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.
| jtsiskin wrote:
| It's not just [] - it's any amount of leading 0s.
|
| But this is exactly the point - if you forgot about proving
| `ToBytes(FromBytes(bs)) == bs`, forgot about this edge
| case, and later tried to prove a function that implicitly
| relied on that fact - Dafny would let you know!
| fluoridation wrote:
| 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.
| Arainach wrote:
| 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.
| mpweiher wrote:
| Yeah, I am also deeply indifferent to these things, even if a
| part of me says "cool".
|
| We have largely solved programming-in-the-small. Making it a
| little bit better is not horrible, but just doesn't move the
| needle much if at all. And you have to consider whether the
| costs are worth it.
|
| I do think that focusing on these things detracts from the
| bigger problems we need to solve.
| pharmakom wrote:
| > how systems interact and their performance characteristics
|
| Let's bring these aspects into the fold of mathematical
| modelling then.
| anonzzzies wrote:
| > 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 wrote:
| 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 wrote:
| > 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.
| kaba0 wrote:
| > 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.
|
| No, that's not even theoretically possible in the general
| case, see Rice's theorem (at least if you stick to Turing
| complete programs), which states that every non-trivial
| (semantic) property of a program is undecidable.
| JonChesterfield wrote:
| The general case is for arbitrary programs. That's not the
| important case. You want to prove things about _this_
| program which you've written, not about all programs.
| ashton314 wrote:
| Type systems push semantic properties into syntactic ones,
| thereby making them decidable. Note that there are halting
| programs which will fail to type check, but that's the
| trade off.
| kaba0 wrote:
| > Type systems push semantic properties into syntactic
| ones
|
| Ordinary types are so-called trivial properties though,
| so Rice's theorem doesn't apply to them.
| consilient wrote:
| This isn't right: `int -> Zero` is an "ordinary" type,
| but certainly does not correspond to a trivial property.
| The reason Rice's theorem doesn't apply to types is that
| they're not purely "semantic" in the relevant sense,
| since they're not fully determined by the language a TM
| accepts.
| kaba0 wrote:
| What type system do you imagine having that type
| signature? Zero being a value is usually exempt from the
| type system (unless we have dependent types, but I would
| definitely not call those ordinary). Of course if it's a
| special type with only a single elem with no relation to
| int, then it is again trivial.
| mrkeen wrote:
| You can get a lot better than trivial. Transactions for
| instance.
| arxanas wrote:
| Rice's theorem states that there is no general procedure to
| determine if an _arbitrary_ Turing machine has some
| property. We are restricting ourselves to programs which
| typecheck under a certain type system, so there will
| certainly be a class of properties it can guarantee while
| still being Turing-complete (such as the bounding of
| memory, CPU, etc.). That is to say that it 's not
| "theoretically possible in the general case," but we are
| willing to work with more specific cases, so it's not
| relevant to invoke Rice's theorem in this situation.
| Ygg2 wrote:
| I think you're being overly reductive:
|
| > Using Rogers' characterization of acceptable
| programming systems, Rice's theorem may essentially be
| generalized from Turing machines to most computer
| programming languages: there exists no automatic method
| that decides with generality non-trivial questions on the
| behavior of computer programs.
|
| https://en.wikipedia.org/wiki/Rice%27s_theorem
| arxanas wrote:
| I don't understand why you say that my comment is
| reductive. It's adding nuance to the topic at hand,
| rather than removing it. The original comment talks about
| a situation where we constrain ourselves to "rigid
| types"; the child comment remarks on Rice's theorem
| having consequences for the analysis of general Turing
| machines; and I remind the commenter that we have already
| restricted ourselves to Turing machines satisfying some
| type system.
|
| Another way to express the same point of view is to say
| that I am arguing that the Curry-Howard isomorphism is
| more relevant to the situation at hand than Rice's
| theorem. (This might be the "promise" that the original
| commenter was referring to.)
| kaba0 wrote:
| > such as the bounding of memory, CPU
|
| I don't think any of those are possible (given that there
| is some construct in the language which will grow the
| memory) - how do you discern how many times will a given
| loop run?
|
| For example, how much memory does this program use?
| int x = input().toInt() for 0..x { //
| something that allocates at least until the end of the
| loop }
|
| And this is the very nicest case of a statically
| verifiably not infinite loop!
| markusde wrote:
| It's not verifiable because you're trying to prove an
| incorrect spec! This program's memory usage is _not_
| bounded above by a constant!
|
| However, many modern formal methods _could_ prove that
| this function uses `f(x)` space, provided the loop body
| is simple enough.
| arxanas wrote:
| For the case of resource usage, you can see work like htt
| ps://link.springer.com/chapter/10.1007/978-3-030-81685-8_
| ... "Synthesis with Asymptotic Resource Bounds" which
| implements bounded resource checking. Of course, there
| are programs it rejects that it can't prove, but this is
| the essence of type systems: if you are willing to
| appease the typechecker, then you can establish facts
| about runtime properties.
|
| For your case, there may be a simpler dependently-typed
| solution: in such systems, you can already say things
| like "given an input natural number n determined at
| runtime, this functions returns a vector of size n",
| which bounds the result vector size. One approach could
| be to disallow explicit memory allocation and require
| passing a memory allocator as a parameter along with the
| associated "request" number bounding how many allocations
| you can do, in a similar dependently-typed way.
| jerf wrote:
| Proofs do not have to be of the form "This will never use
| more than 64 bytes of memory". You can prove that
| something will use x times 32 bytes of memory, or a
| polynomial value based on x, or whatever you have. Then
| you have to decide if that meets your needs or not.
|
| But this is also where they get tricky. You can have a
| proof that a particular sort function will never use more
| than twice the memory of what you pass in, and then you
| can combine that with a proof that some other bit of code
| will never have more than 10 elements, and that produces
| a proof that you only need 20 element's worth of memory
| for that upper function... but across an entire program,
| what sounds cute and useful in my little example here
| becomes its own monster of complexity. So far it is not
| yet clear to me that it constitutes an improvement on the
| underlying program.
| jfoutz wrote:
| I'm going to assert, you can calculate how much memory
| you'll need as soon as you see x. (maybe it's gnarly and
| complicated, but you can put an upper bound on it).
|
| That number can be calculated at runtime. The program has
| access to the number, and you can make a choice about
| running that for loop or not.
|
| The nifty bit is, the memory use information can be
| encoded in the type. the function has access to its type
| information. The compiler checks, and can make guarantees
| about your guard strategy - the actual values of
| available memory, and how much memory operating on x
| requires are only known at runtime. But the compiler can
| be check at compile time that the strategy is sound.
| maybe you have 5 bytes, maybe you have 5 gigs, who cares?
|
| This can all be done without fancy languages, just write
| good code.
|
| It's pretty nice to be able to throw more allocating
| function calls in the for loop, and have the compiler
| recognize that you're using (maybe) more memory, but your
| guard strategy is still good.
| markusde wrote:
| This is a good but also misunderstood point. It is true
| that you can't automatically do this in general. However,
| expressive enough type systems can contain human-written,
| machine-checked proofs of (models of) these properties. I
| think the jury's still out on whether or not humans or
| machines are better at coming up with proofs, but computers
| are decisively a lot better at checking them than we are.
|
| The way I see it formal methods not a holy grail where we
| don't have to think about the code we're writing anymore,
| but it is a very strong next step from "I wrote this code
| and here's why I think it's right" to "I wrote this code
| and here's a machine-checked proof that it's right".
| Effective automation can make that step easier to take in a
| lot of real-world cases.
| kaba0 wrote:
| It's not about automatically doing it -- it's about for
| many cases there _can't exist a proof_. And it is not
| even some theoretically interesting but never happening
| case, but quite trivial programs will quickly come to
| this state. Sure you can restrict some things, like
| boundless loops, but the "beauty" of complexity and the
| limit of our very mathematics won't disappear, unless you
| go to too trivial systems which are useless. See my other
| comment for an example.
|
| I remember there being an analogy between Godel's
| incompleteness theorem as well, which is also only true
| to "expressive enough" systems (where you can basically
| do integer math) -- but I may be talking completely out
| of my arse at this point.
| markusde wrote:
| I get your point, and I agree with it too. My comment is
| (trying to) say that in those cases we don't know that
| humans are any better!
|
| Your other comment has some problems, but a better
| example is
|
| fn collatz(mut n: bigint, mut v: Vec<...>) {
| loop { n = { if n%2==0 then n/2 else 3\*n+1
| }; v.push(...); }
|
| }
|
| As far as we know, we can't bound the memory usage of
| this program: and if any FM can do it as well then
| there's a million bucks on the table. But so far no human
| can do it either! And if your program relies on this
| program using bounded memory, from an engineering
| perspective you're kind of SOL no matter what.
|
| On the other hand, if you're writing programs which
| humans are pretty sure they know why the properties they
| want hold (as we usually try to do, anyways), then
| translating this into a machine-checked proof can give
| you a lot more faith that the property actually holds and
| possibly even find flaws in your reasoning/implementation
| if there are any!
| kaba0 wrote:
| Yes I agree with you on every point (though didn't want
| to use the "heavy gunner" Collatz as an example :D). I'm
| not against dependent types, and I eagerly await what
| future might they bring. But at the same time I think the
| best solution will be to "fight on multiple fronts", and
| improve our type _and_ test systems. There are very
| interesting ways to systematically test every _kind_ of
| input (greatly reducing the input space) that has a
| distinct code path (and it can find a minimal
| reproducible error case!).
| reuben364 wrote:
| Well one thing programmers do often due to the complexity
| of formal proof is random property testing instead.
| Mathematicians do so too, which is why the Collatz
| conjecture is a conjecture in the first place. There is
| an alternative to Software Foundations that uses
| randomized property checking. It would be interesting to
| have a hybrid system where we independently give
| specifications and then decide whether we wanted to
| formally prove them or just do tests instead.
| jerf wrote:
| "(at least if you stick to Turing complete programs)"
|
| Many people interesting in this sort of formal proof
| community are actually perfectly willing to eject that.
| There's been a lot of interesting research into it. I think
| you can also ring-fence chunks of a program as being non-
| Turing complete and prove things about those chunks even if
| the program as a whole is Turing complete.
|
| That said, so far everything I've seen them produce
| involves a level of programming difficulty comfortably
| above writing real-world code in Haskell. For example, you
| do not have to learn category theory in the slightest to
| learn Haskell, but you will be learning a lot of real
| mathematical theories, of which group theory is probably
| one of the easier ones, to use these systems. They're
| working on that issue. But it has a long ways to go and it
| is not clear to me that the gap between these systems and
| the "programmer on the street" is anything that can ever be
| solved.
|
| Or, to put it another way in more engineering terms, I do
| not question the advertised benefits when advocates like
| the original author pitch them. They're real and exist in
| real, concrete systems that you can use today. However, the
| _costs_ are grotesquely undersold. I 'm not sure even the
| advocates really understand how far out of the loop they
| are on the costs of their systems. So far the costs end up
| choking you out on systems that conventional programmers
| would consider tiny. My browser may not be mathematically
| proved to not have security vulnerabilities, and it's
| certainly not free of bugs, but in the meantime,
| conventional programming has produced it and it's out there
| in the world bringing benefits today, not in however many
| decades or even _centuries_ we are away from having
| something like a browser-sized program come with proofs of
| security and resource usage.
| thesuperbigfrog wrote:
| "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/cont...
|
| The SPARK subset of Ada also does static proofs / formal
| verification:
|
| 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/
|
| Maybe one day Rust will have formal verification too?
|
| Work is under way: https://alastairreid.github.io/automatic-rust-
| verification-t...
| redjamjar wrote:
| Yeah, SPARK/Ada is a comparable system to Dafny. I agree with
| that! Also, Frama-C and a bunch of other more esoteric research
| languages as well.
| perlgeek wrote:
| In Eiffel at least, the contracts are checked at run time,
| whereas in Dafny it seems that it's verified at compile time.
|
| I think (but I'm not sure) that Eiffel disables recursive
| contract checking (so checking a contract of a function used
| for checking the contract), so you could put the check for the
| inverse in each of the function's post conditions, but it would
| be quite the performance hit to verify it at each call.
| jakuj wrote:
| 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
| lionkor wrote:
| > Rust has Design by Contract capabilities via the contracts
| crate
|
| And C++ has reflection using boost ;)
| thesuperbigfrog wrote:
| Contracts for C++ have been proposed:
|
| 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/p05...
| zoogeny wrote:
| 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.
| [deleted]
| PsylentKnight wrote:
| > 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.
|
| You seem to be implying Esperanto's lack of popularity is
| related to its regularity, but I don't think it has anything to
| do with that - it comes down to network effects. It's not an
| official language in any country. There are very, very few
| native speakers of Esperanto. Of those blessed few, they
| obviously have at least one other native language, otherwise
| they'd be completely cut off from society.
|
| And by the same token, English is popular as a second language
| due to network effects and the benefits learning it can confer
| (read: better economic opportunities) and little to do with its
| regularity. A lot of people have had the experience of learning
| a bit of Spanish and realizing that English's spelling system
| is atrociously irregular and we gain nothing by having so many
| spelling rules that have so many exceptions they can hardly be
| considered "rules". In fact, English's spelling used to be much
| more regular, it's just that our pronunciations have shifted a
| lot over time while the spelling has remained relatively
| static.
|
| This is all tangential to your larger point, I just like
| talking about this kind of thing.
| nine_k wrote:
| 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.
| valenterry wrote:
| react is not an example for a library that is supposed to be
| or even possible to be used in a pure functional programming
| way.
| nine_k wrote:
| Look, you have a large stream of pure functions that
| exchange immutable data. There is a place where you can
| thread in the effects, and it's not _entirely_ like using
| >>=, but after it, it's immutable data and pure functions
| again.
|
| It's _very_ different from jQuery and the callback hell, or
| from any two-way bindings all the way to Visual Basic.
|
| It teaches you to _value_ immutability and purity, to crave
| it (then comes Ramda, etc).
|
| Also, Promises are not entirely monadic, and `async` is not
| entirely the do-notation, but you can use a lot of monadic
| approaches, and reap some of the benefits.
| valenterry wrote:
| > and it's not entirely like using >>=
|
| Exactly, and that's why it is not pf. It's really as
| simple as that.
|
| It's also not as if it would be theoretical distinction
| that has no meaning for praxis. It does. For instance,
| since I cannot control the execution of React's cycle
| (including rendering) it becomes hard(er) to do certain
| kind of page animations that should happen between
| renders.
|
| > It's very different from jQuery and the callback hell
|
| Yes, it is nicer to use. But it is not pfp-style.
| nine_k wrote:
| What would you suggest as a pure enough example of FP
| GUI? Anything besides Elm, I mean? :)
| valenterry wrote:
| I have never worked with one professionally (I rarely do
| frontend work anyways) and for my own projects I used
| react, dirty and productive as it is. ;)
| adamwk wrote:
| Right, there's definitely functional-inspired bones (e.g.,
| a view is a function of state); but every hook is a side
| effect, even the redux ones.
|
| And I don't think it would even be improved by being pure;
| Elm has much more boilerplate to do similar things.
| valenterry wrote:
| haha, Adam from SM, is it you?
| WorldMaker wrote:
| React can still be viewed as functional programming if you
| assume Hooks operate in/on/with an unnamed/untyped monad.
| ("Pure" of course depends on your take of monadic
| programming from there.) It might be nice if that monad
| were better typed and/or at least parametric (reflected in
| input or output parameters), but it all exists in an
| untyped language to begin with, so it is mostly fine how it
| works right now. Mostly.
| c_crank wrote:
| JavaScript has never been and probably never will achieve any
| sort of purity due to the design decisions made in its debut.
| Frameworks can only paper over that so much.
| valenterry wrote:
| I mean, there are fp-ts and ts-effect. Sure, internally
| they do nasty things, but at least as a user I think it's
| possible to write pf or at least mostly pf code. (without
| commenting on whether that is a good idea or not)
| rirze wrote:
| Funny enough, Japanese is incredibly fun and enjoyable when
| you use dialects and break the syntax to be "artsy"
| nine_k wrote:
| But even that does not increase the number of irregular
| verbs past two and a half (kuru, suru, arieru). I don't
| know enough Japanese to say if one can invent forms like
| "swole" or "boxen" in it, so that they would remain
| recognizable.
| dunham wrote:
| The dependent languages are interesting. But the theorem
| proving is not easy, and probably overkill for a lot of
| applications. Even for stuff like boundary conditions for
| binary search, which could be checked with Hoare logic, I
| usually handle by stealing the implementation from the Go
| standard library (so I don't have to think about it).
|
| Last year I did advent of code in Lean4. I had written a heap
| implementation that I didn't end up using. As an exercise, I
| went back and added proofs for my indicies and a termination
| proof. I got the termination proof down to `0 < 0` and realized
| that I had an off by one error (I'd used the math for a 1-based
| array with a 0-based array).
|
| My take-away was that this stuff can catch real bugs, but also
| that people are not going to do this stuff day-to-day. Maybe
| some equality saturation thing will make it possible for the
| compiler to sort out the proof in most cases. If the compiler
| can hit 80%, you could use it as a linter. (If you want
| something stricter, you can do totality checking but have
| escape hatches like Idris' assert_total / assert_smaller.)
|
| > 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.
|
| The structured vs unstructured thing is also interesting. I
| came to a similar conclusion years ago. I'd written some
| heuristics to pull recipes out of web pages, and also use
| embedded microdata on some pages. I found I got better results
| with my heuristics because of bad encoding of the structured
| data. E.g. a web site was missing entire ingredient blocks in
| their encoding because their process / data model didn't
| accommodate recipes with multiple ingredient blocks.
| thr_ddv wrote:
| >The compiler still cannot tell when our loops will terminate
| (yes, this is possible). while(n <
| busy_bever(10)) n++
|
| Tell me when my loop terminates.
| littlestymaar wrote:
| That's not a very good exemple because with BB we know the
| code terminates, by definition. The canonical tong-in-cheek
| argument is to use the Collatz conjoncture instead (but even
| that isn't a good example in practice:
| https://news.ycombinator.com/item?id=21440306)
| thr_ddv wrote:
| I'm not asking if it terminates, I'm asking when it does.
| After all it's not much use if the number overflows the
| universe.
| littlestymaar wrote:
| But that's not something these kinds of tools are
| supposed do, even with trivial functions... These tools
| have no idea about the run-time (and there's no way they
| coule, since it depends on the load you put on the
| hardware in parallel of running your program)
| redjamjar wrote:
| I agree. There are tools though which are specifically
| for determining worst-case execution time for e.g.
| embedded systems which can actually give accurate timing
| information (upto a point).
| nine_k wrote:
| For practical reasons, it's enough to prove that it takes
| longer than some upper bound, say, 10 ms. The rest is not
| important.
| redjamjar wrote:
| Yeah, so these tools will not tell you how long it will
| take to terminate --- only that it will eventually. In
| the vast majority of cases, that is what you want to
| know.
| rockstar-guy-23 wrote:
| while(calculate_pi_stream(10 /* substring length */) !=
| 0987654321);
| nine_k wrote:
| I remember there was a theorem that one can find an
| arbitrary substring in a long enough output of infinite
| (stationary) random process. I also suppose that a decimal
| representation of pi _may_ count as one, then your function
| provably terminates.
|
| But this is of a theoretic interest. In practice the
| verifier says: "I can't prove that this function will
| terminate within (some reasonable window), program
| rejected". And this is what's actually needed: a program
| that provably has certain properties, where an automatic
| proof is tractable.
| xigoi wrote:
| It is currently not known whether p is a normal number
| (that is, its representation in any base contains any
| finite sequence of digits with the same density as in a
| uniformly random string of digits).
| redjamjar wrote:
| Haha, yeah ... this one you would have a very hard time
| with :)
|
| Hopefully, though, termination of your program does not
| depend on this ... otherwise could be a long wait!
| jjnoakes wrote:
| > Tell me when my loop terminates.
|
| I think the point is that even though one can't determine
| loop termination for all loops (easily provable), there are a
| huge number of useful loops that do useful work and for which
| you can prove properties like termination (and other static
| properties).
| redjamjar wrote:
| > there are a huge number of useful loops that do useful
| work and for which you can prove properties like
| termination
|
| Exactly! If the loop doesn't terminate, then you obviously
| cannot show it. But if it does, then you should be able to
| (even if that requires some changes to help the tool)
| jjnoakes wrote:
| > If the loop doesn't terminate, then you obviously
| cannot show it.
|
| I don't think this is true for all loops either - some
| can be proven to never terminate, just like some can be
| proven to terminate. And some can't be proven either way.
| redjamjar wrote:
| Yeah, ok that's fair enough!!
| jcranmer wrote:
| Assuming you meant 'busy_bever' to implement the busy beaver
| function, said function is in fact not a computable function,
| which means you can't write it down in a programming
| language.
| Smaug123 wrote:
| This is true but somewhat misleading. The nth busy beaver
| numbers are known for n <= 4. It's within the bounds of
| possibility that we will some day learn the nth busy beaver
| numbers for n <= 10. (What we _can_ say is that the parent
| 's loop will never terminate for any known definition of
| "ever" that pertains to the physical universe.)
| a1o wrote:
| I think C++ may get something like this with contracts, which
| hopefully makes in C++23!
| agentultra wrote:
| 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.
| sn9 wrote:
| Talk link: https://youtu.be/k6rY5Mvx84E
| practal wrote:
| 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 wrote:
| Well you can encode any logic you want in dependent types, so
| yeah probably!
| practal wrote:
| 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.
| iasdj38103 wrote:
| Amazon uses Dafny to ensure that their authorization engine makes
| correct decisions: https://www.amazon.science/blog/how-we-built-
| cedar-with-auto...
| looperhacks wrote:
| > 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?
| benburton wrote:
| Thank you. I thought I was going crazy.
| two_handfuls wrote:
| 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
| IshKebab wrote:
| 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 wrote:
| > The halting problem has almost no practical relevance
| because we don't really care about the general case.
|
| Yup, agreed
| fjfaase wrote:
| 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
| skydhash wrote:
| You may want to do a Find and Replace (piramid to pyramid).
| redjamjar wrote:
| 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.
| tromp wrote:
| 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
| sn9 wrote:
| And a whole textbook was recently published as well:
| https://mitpress.mit.edu/9780262546232/program-proofs/
| ComputerGuru wrote:
| 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
|
| _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 wrote:
| 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 wrote:
| > 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 and in
| 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!)
| galkk wrote:
| 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?
| apatil wrote:
| 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 wrote:
| 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.
| FrustratedMonky wrote:
| 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.
| janAkali wrote:
| 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
|
| [1]https://nim-lang.github.io/Nim/drnim.html
| manaskarekar wrote:
| > 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 wrote:
| 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.
| lolinder wrote:
| Dafny also originated in MS and initially targeted .NET.
|
| https://www.microsoft.com/en-us/research/project/dafny-a-lan...
| scythmic_waves wrote:
| 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 wrote:
| 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.
| lenocinor wrote:
| 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 wrote:
| I'm trying to learn Lean and like it, but it's terribly
| lacking documentation.
| toastal wrote:
| Why3 'extends' OCaml with similar features as well
| sn9 wrote:
| There's actually a brand new textbook on using Dafny at the
| level of an early undergraduate course:
| https://mitpress.mit.edu/9780262546232/program-proofs/
| Hardliner66 wrote:
| People always think that using some sort of formal verification
| is overkill, but then they end up hunting bugs for months that
| would be trivially detectable in such tools.
|
| Formal Verification tools allow you to write a specification in
| a common language, that can be checked by a tool. Every time
| the spec changes, you can instantly verify that all invariants
| still hold.
| lenkite wrote:
| I wish something like Lamport's TLA+
| (https://lamport.azurewebsites.net/tla/tla.html) was
| supported in modern language compilers - perhaps with
| annotations/macros and a mini formal DSL.
| mrkeen wrote:
| And types too :)
|
| I know many words have been spilled over why it shouldn't
| have them, but I remain unconvinced.
|
| I modelled a trivial traffic light system to make sure the
| cars and pedestrians didn't have "green" at the same time.
| And they didn't, because they had "green_light" at the same
| time. Oops!
| abathologist wrote:
| It's still in pretty early development, but you may be
| interested in https://github.com/informalsystems/quint
|
| > It combines the robust theoretical basis of the
| Temporal Logic of Actions (TLA) with state-of-the-art
| static analysis and development tooling.
|
| And it is typed ;)
| Hermitian909 wrote:
| It's a tooling problem. Nearly every comment I read about
| formal verification being overkill are about proposal to
| incorporate existing formal verification tools into existing
| workflows. It is not easy to get an organization to adopt
| TLA+ in a way that's useful for almost any problem.
|
| Add a language feature like the above to TS and you'd see
| adoption overnight. Pretty much everyone is happy to let
| their build system add additional correctness guarantees if
| its fast enough.
| anonzzzies wrote:
| Yes, lot of formal verifications are (almost) free and most
| others are not. But if you at least take the free ones, why
| not...
___________________________________________________________________
(page generated 2023-06-29 23:01 UTC)