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.
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.
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.
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)
You can actually type JS to be incredibly more strict than TS does if you have the motivation. It still won’t be impossible to reach runtime errors, but it can be very close to “you really have to try and mean it”.
> Loving flaws like buffer overflows looks more like a Stockholm syndrome to me:
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 )
But even that does not increase the number of irregular verbs past two and a half (くる, する, ありえる). 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.
You can invent a lot of things in written Japanese using textspeak and other alphabets.
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.
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.
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
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. ;)
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.
I don't know. I haven't used hooks much, but while you might consider it pure-functional in a way within a component that uses (a single) hook, I think using multiple hooks and having everything integrated is certainly not pure-functional.
It's easy to test right? Can you replace calls/expressions with their result-value? If no, it's not pure-functional.
Like I said, I don't think it counts as "pure" functional because it is heavily monadic. Many Haskell users still think non-monadic code is "more pure" than say anything that uses the IO Monad and Hooks are "worse" than the IO Monad. (Especially some of the "Suspense" project Hooks which combine IO and Futures and State and more from a Haskell standpoint into one super weird monad.)
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).
> You can certainly replace most hooks with static return values.
"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.
Hooks definitely build a complex data structure. They don't actually run immediately/imperatively. Even `useEffect(callback, undefined)` (no defined dependencies) which gives the illusion that it runs "immediately" on every render is still an illusion of sorts and there's a complex scheduler apparatus feeding on the data structures under the hood that useEffect builds.
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 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.
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.
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).
> 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)
> 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.
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.
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.)
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)
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)
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).
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.
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.
It is currently not known whether π 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).
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.
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.
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.
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.
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!
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.
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.
IMO this is going up the spectrum from runtime checking to static checking, and it becomes more and more useful when you are writing libraries for mass consumption or working in large codebases with a lot of developers. I wish I had stuff like this at my last job, so much boilerplate to basically guarantee similar stuff statically would be replaced by a few one liner 'ensure' clauses.
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.
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.
> 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.
> 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.
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.
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!
For the case of resource usage, you can see work like https://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.
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.
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.
> 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.
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.)
"(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.
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.
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 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.
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!
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!).
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.
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.
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.
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.
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.
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?
> 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.
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.
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…
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.
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.
> 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!)
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.
> 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.
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.
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.
> 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?
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.
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.
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.
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.
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.
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.
Intrusive linked lists trade away simplicity and ease of refactoring for better memory characteristics. There's a huge amount of code where that trade is a terrible deal. Obviously you shouldn't use ordinary linked lists deep in the guts of an OS kernel or automated trading system but claiming that they're useless is absurd.
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.
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.
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!
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.
I was coming to say almost the exact opposite. `ToBytes(0)` should be equal to the empty array. This seems like the more natural representation, at least to me.
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.
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.
Interestingly the postcondition does not prove that the GCD implementation is correct and by extension does not prove Bézout's identity.
Stating that some value is the gcd is surprisingly tricky. Once you have proven that Bézout's identity holds for your function you could prove it is the actual gcd by showing it is a divisor for both a an b. Assuming I understood the notation correctly that would give something like the following
lemma euclid_gcd(nat: a, nat: b)
ensures (a % GCD(a,b)) == 0
ensures (b % GCD(a,b)) == 0
{ }
I'd be curious to know if it can prove this. Note that this would still not constitute a proof of Bézout's identity, as it uses it to define what the gcd is. Thankfully defining the gcd using Bézout's identity is pretty common nowadays, as it allows for a useful generalisation of the concept.
I think even your example is not actually proving GCD, just that the result is _a_ common divisor. E.g. it would succeed if GCD(a, b) = 1 for all a, b.
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.
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.
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.
well this is a surprise, He was my old lecture (one of the best at my university tbh). Was always obsessed with formal verification. I remember him trying make us use a formal verification programming language he created called whiley, Which was a java based language and was pretty terrible and filled with bugs lol but had some cool ideas in it
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.
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.
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.
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
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.
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.
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?
Cool article. This language looks really interesting. The only problem though is, how do I use it? The majority of the programming I do in my daily life revolves around performing actions in a database based upon the contents of HTTP requests. There's lots of amazing programming languages out there, however there don't seem to be any really pushing the boundaries for web programming.
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?
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:
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.
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.
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').
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.
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.
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.
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.
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.
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.
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.
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.
That's because monads are way more general than promises. Explaining how to use Maybe to write total functions is just as easy as explaining promises, if not easier.
So long as you're using a single Monad like a black box. Haskell people repeatedly fail when trying to generalize them or explain the underlying premises.
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.
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.