Programming languages going above and beyond
whileydave.com
whileydave.com
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.
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.
And I don't think it would even be improved by being pure; Elm has much more boilerplate to do similar things.
It's easy to test right? Can you replace calls/expressions with their result-value? If no, it's not pure-functional.
You can certainly replace most hooks with static return values. Many hooks are heavily memoizable and in turn heavily memoized which is how they find their performance in practice.
Multi-hook interactions generally follow a lot of the laws of monadic binding and a lot of the "hooks rules" aren't that strange in terms of monads: monadic binds have sequencing that matters (and dependencies you might track). The order of hooks matter in the same way that the order of IO binds or the order of Futures/Promises awaits.
Again, it is certainly hard to call it "pure" functional in most ways, it has a lot of impurity, but it is certainly "deeply" functional. There's not really a better paradigm to call what is React is doing with Hooks than "functional programming". The language of monads is somewhat helpful in reasoning about how Hooks work and where they sit in the paradigm. They definitely make everything a bit more "impure", especially from the strict mathematical sense of "pure functions are entirely dependent on their parameters". Especially with Hooks not being represented parametrically (which I did mention I think can be something of a problem and I wish wasn't the case).
"most" is not good enough. The idea of PFP is precisely that there is no exception, otherwise all guarantees are void. If I cannot rely on an expression to be referential transparent, then it means I have to look into to find out - and with that, the advantage of PFP goes through the window.
> The order of hooks matter in the same way that the order of IO binds or the order of Futures/Promises awaits.
The difference is that if you create an effect in a PFP style (like in Haskell), the effect itself doesn't do anything. You can now combine that effect with another effect in some way, e.g. by sequencing, which means first effect A and then afterwards effect B is executed. Yes. But what you get back is, again, an effect that doesn't do anything. So what you need to do is to build a datastructure of effects.
Do you do that with hooks? I don't think so. With hooks, you call one, then call another, and yeah, the result depends on the order just like with an effect monad like IO. But the difference is that once the line of code that calls the hook is executed, something happens and the world has changed. This is not true when you can the line of code that builds the datastructure for the effect execution.
You would have handle hooks like promises for this to work in a PFP way. But maybe I misunderstand and you can clarify it with a code example?
Otherwise, I just think it's about terminology. I agree that there is a relation between the two things, but we shouldn't give it the same name, because it is still not the same concept.
The data structures that Hooks build in React gets built in a strangely bound, somewhat liminal `this` space so it effectively "disappears" in JS. That's certainly not how I would have built it. You are right that I probably would have used something more like JS Promises, given the choice. But I didn't build React's Hook systems, I'm just an outside critic. I'm very happy to agree that use of `this` bound things is about as impure functionally as you get in JS. (That said, it is a very JS solution that predates React and gets to old debates of whether or not JS is truly "OO". Prototypical OO is a gray space between OO and functional paradigms.)
Hooks are never imperative, even in the most complex multi-hook components. They use and build data structures. Those data structures are mostly hidden from view and hard to inspect, but they exist.
But you don't. It is react that builds the datastructure in the background, not you that builds and controls it. Hooks might be declarative, but this is actually orthogonal to being pfp or not.
All of that is totally fine btw., there is no need for everything to follow a pfp style. It's a tradeoff. But we shouldn't call something pfp that isn't, even if it is closely related.
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.
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.
Spoken Japanese you can't break the rules because everyone else instantly becomes unable to understand you. They barely use local accents/dialects in media because of this.
Only if you are the developer (victim ) it is fun to work with buffer overflows if you are the security researcher (law enforcement) or a hacker (kidnapper )
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.
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.
while(n < busy_bever(10))
n++
while(calculate_pi_stream(10 /* substring length */) != 0987654321);Hopefully, though, termination of your program does not depend on this ... otherwise could be a long wait!
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.
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).
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)
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.
lemma LemmaFromToBytes(v: nat)
ensures FromBytes(ToBytes(v)) == v {
// Dafny does all the work!
}
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.
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.
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!
> 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 ;)
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.
I think we will see this feature added to production languages in 3-20 years, hopefully sooner. I think Eiffel had this feature too with their program by contract feature?
It's basically baking in more and more parts of unit tests into the language itself, and a one liner 'ensures' clause is way more concise and stronger of a test than a unit test you have to run separately or an assert that does checks at runtime.
The key issue with static verification is making sure it doesn't get in the way of build speeds, execution speeds and binary size.
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.
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.
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?
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.
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.
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
}
However, many modern formal methods _could_ prove that this function uses `f(x)` space, provided the loop body is simple enough.
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.
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.
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.
> 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.
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.)
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.
I remember there being an analogy between Gödel’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.
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!
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.
Ordinary types are so-called trivial properties though, so Rice’s theorem doesn’t apply to them.
> Of course if it’s a special type with only a single elem with no relation to int, then it is again trivial.
No, it isn't. "Trivial" in the context of Rice's theorem means either true of all Turing machines or false of all Turing machines.
Let’s bring these aspects into the fold of mathematical modelling then.
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.
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.
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!)
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.
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.
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...
And C++ has reflection using boost ;)
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...
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.
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?
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
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.
Yup, agreed
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.
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.
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.
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.
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!
1. The implementation of `FromBytes` works properly only if the base case returns 0 for the empty array. So you already have, for free, `FromBytes([]) == 0`. You might as well use it.
2. `LemmaFromToBytes` currently requires the somewhat awkward and complicated `requires |bytes| > 0 && (|bytes| == 1 || bytes[0] != 0)`. We need to restrict this to only allowing non-empty arrays. And then we need to restrict it to not allowing leading zeros on arrays, except if the array is of length 1 and then we do allow a leading zero. If we represent 0 as `[]` instead of `[0]` then this all simplifies down to something like `requires |bytes| == 0 || bytes[0] != 0`. We allow arrays of any size and we never allow leading zeros on any array, which is easier to express.
3. Currently `ToBytes` has an `if-else` at the end and requires repeating the code `[byte]` in both branches. That's obviously not a lot of repetition but wouldn't it be nice to eliminate that? If we change the beginning to `if v == 0 then []` then we can replace the `if-else` at the end with just `ToBytes(w) + [byte]`. And we can get rid of the `ensures |r| > 0`. Then the structure of `ToBytes` and `FromBytes` more closely mirror each other, with the base cases being "the same".
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.
My point is that for most use cases formal verification by itself is less important than all the other stuff.
[1] https://www.doc.ic.ac.uk/~scd/Dafny_Material/Lectures.pdf
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 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.
Yeah, sorry --- that is a typo.
Love the type checking, which I think is better than Rusts. But since I think Rust will win the market, I hope it improves.
https://www.microsoft.com/en-us/research/project/dafny-a-lan...
Could you please elaborate on this? What specific stuff are you suggesting that F# does so well?
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.
You can, but you don't have to...
Well, nobody apart from you did...
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.
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
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.
lemma LemmaFromToBytes(v: nat)
ensures FromBytes(ToBytes(v)) == v {
// Dafny does all the work!
}
---
How long does it take, do we rely on caching compilation results here? Is it iterating through all values?
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').
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.
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.
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.
I do see (irl) that it improves the odds though.