The example given with the `Point` struct is interesting. As a self taught developer with admittedly little language design knowledge, it almost seems like unit tests without all of the boiler plate.
For instance, the `is_diagonal` function provided as the "correctness checker" looks to me like something that would be in a unit test for the `double` function. However, I think it goes a little bit deeper than that. In a unit test, you are somewhat required to pass specific values to the constructs you are testing. The given example is more complete than a unit test in that it doesn't just test for the correct value being produced by the `double` function when given specific values, it actually checks all possible outcomes by asserting that the `double` function always produces a `Point` where `p.x == p.y`.
Given that the example is relatively trivial, I would like to see how this would work for more complex functions and structures.
Something in between what you describe and what the article does with F* would be Haskell QuickCheck or Scala ScalaCheck [1] testing where the framework determines the test parameters for your tests.
Does the linked case study[0] help at all? It's real code that already had debug assertions that acted as a postcondition. It was than formally proved that those conditions held (or didn't hold in one case) for all the relevant functions.
It does help. what I find interesting here is that the prover was able to find a potential bug that the test cases were not able to find. That's powerful.
There is a lot to be said for understanding types as a kind of test, but performed at development time rather than runtime. And valid for all possible inputs, not just some specific ones.
> There is a lot to be said for understanding types as a kind of test, but performed at development time rather than runtime. And valid for all possible inputs, not just some specific ones.
The types you write in code describe program properties to be proven and the type checker tries to create a proof that those properties are true for all inputs and outputs. Tests as you say only check a small number of inputs/outputs in comparison. It's very similar to mathematics where checking if a conjecture holds for a few values is a poor substitute to a rigorous proof.
The insight that proofs and types are analogous is an interesting one, but all of this (the writing, the math, and the code) strikes me as fairly impenetrable. It does not surprise me that this is rarely mentioned in industry.
> The insight that proofs and types are analogous is an interesting one, but all of this (the writing, the math, and the code) strikes me as fairly impenetrable. It does not surprise me that this is rarely mentioned in industry.
Yes, it does look impenetrable but the high-level idea is fairly intuitive and it's the foundation of many formal proof assistants (e.g. Coq, Idris).
I see comments quite often where people suspect some vague links between writing maths proofs and type checking computer programs so I think it's worth knowing a very deep connection has been known about this and researched for decades.
The simplest place to start, in my opinion, is [0]. If you understand that, then the fact that types are propositions and proofs are values of those types seems pretty obvious.
Property-based tests are really practical and will find bugs unit tests don't, but type checking is an exhaustive proof that the properties you've expressed with types hold for all inputs/outputs. A key point though is the type systems of most mainstream languages don't let you express complex program properties (e.g. the input list must be sorted), so your only option is to use unit tests or similar to check those.
Yes, I know that. However, they don't need to be exhaustive. They are very effective at uncovering any bugs using a statistical approach at even very reasonable levels of iteration. And nothing precludes you from running them 24/7 in the cloud.
I wouldn't say using a "unit test" is ever really a viable option for me. Property-based tests subsume unit tests.
There is a problem though that Turing completeness allows for inconsistencies. i.e., you can technically "return" a bottom type in these languages by looping forever. That is actually why Coq is not Turing complete since Coq is primarily used for theorem proving and less for programming.
Turing completeness as the ultimate measure of expressiveness for programing/logical systems is a myth. I argue every interesting program you may want to write is either terminating, co-terminating or step-indexed. Terminating programs are well understood (using structural recursion, inductive data, etc). Co-terminating programs are stuff like servers/daemons/guis: you want them to (possibly) never terminate and always progress (respond) in finite time, these are expressible using coinductive data, structural corecursion etc. And lastly, if you have a program which may hang for an indefinite amount of time, you really should put a timeout (or heck, a co-timeout, eg some kind of heartbeat), that's step-indexing.
So no, Coq and other "total" programing languages (agda, idris, F*) may not be turing complete in the usual sense because the two things are contradictory, but they are much better: you can simulate a turing machine as a server which will be provably always making progress in finite time.
This understanding shows also the flexibility that unit tests brings to the development cycle: contrary to type checks, they can be temporarily disabled so as to shorten the iteration loop when necessary, and re-enabled after adjustments have been made.
(Contrast with long compile times which are incompressible)
The rust compiler will help you avoid a lot of common runtime errors. It comes at a cost of extra development time. The Rust philosophy values code correctness over developer efficiency.
I'm confused by this sentiment. How efficient is a developer when producing things that are incorrect? Unless the goal is produce incorrect things, which seems unlikely.
It seems like the philosophy prefers knowing ahead of time what's wrong over discovering it incidentally, and probably accidentally, after the fact.
There are many times where you don't need 100% correctness (e.g. prototypes, or edge cases that in practice are never hit) - I'd say it might be more accurate to say that Rust makes it harder/less convenient to take out technical debt.
I discovered a bug that could potentially be triggered in the codebase where I work, but never has. It's about 5 years old.
You don't actually always need technically correct - sometimes you want practically correct, where "practically" covers a huge spectrum.
Because if say, 75% of your time is spent debugging in an "regular" language then you really aren't saving much time by reducing the amount of code you must write.
If we could reduce programming to typing in mostly correct code then software development will be much faster, even if the code we type is 50% longer.
That 75% of the time is spent with a mostly functioning program though. There are a lot of cases where getting something now is worth overall spending 10x as much time getting it right latter.
Of course everyone wants the best of both worlds: everything now, zero bugs. Fast, cheap, right: pick two applies despite everyone wanting all three.
> I'd say it might be more accurate to say that Rust makes it harder/less convenient to take out technical debt.
I'll disagree with this one. Refactoring old and rarely-touched code is bliss when working under a strong type system, at least relative to dynamic or weakly-typed languages. The key to the timely resolution of technical debt is to allow things to be updated in piecemeal rather than in one enormous burst; this requires solid abstraction boundaries and encapsulation, both of which are provided by types (in addition to other features of a language, such as a module system). The fact that Rust so heavily discourages global state is another point in its favor.
We can agree that there are contexts where correctness is less important than velocity, e.g. prototyping, though languages that front-load correctness at the expense of velocity are going to produce less technical debt in the first place, because the debts can be paid off before they accrue interest.
This tradeoff obviously can’t be evaluated without considering quantities. What percentage of your bug load is reduced, at the cost of how much development time?
That said, it’s not that simple. There are threshold effects (more than X amount of time = your company is dead) and intangibles (how do you feel while programming).
But anyone making a blanket statement without considering these things is participating in a dumb internet argument.
>I'm confused by this sentiment. How efficient is a developer when producing things that are incorrect?
How is this confusing?
If it takes you 2 weeks with language X to write a sloppily written app, that works 99% of the time but has some errors -- and 2 months with Rust to write a version of the same app that has no errors, what you'd you prefer?
Ever heard of "time to market"? What good it would be if you get it 100% right, and your competitor has their app already out, and captured all your potential customers?
And even if time to market is not involved, would you really care for some occasional errors, if you get the majority of the functionality you want working just fine?
If you build pacemakers and airplanes, the answer is yes.
If you build regular websites, apps, and scripts, the answer might very well be no.
That's the case, just the numbers (2 weeks, 100% etc) are made up.
Yep. This is also why this is such a hard discussion to have: there’s no good way to get those numbers, and they vary by developer. What if that two months drops to three weeks, because you’ve put in the time to learn Rust better? What if that time to learn is a year? What if that 1% failure leads to six more months of developer time to fix?
It’s a large, multi-variable problem. This is why it’s great that we have so many languages!
> What good it would be if you get it 100% right, and your competitor has their app already out, and captured all your potential customers?
A constant stream of bugs have driven customers away before too, so if you're waiting in the wings with a bug-free/verified version of your competitor's program, you have a real shot at stealing their customers. First mover advantage is important, but so is quality if marketed properly.
I admit personally I'm inclined to agree with coldtea. But one example where I think the stability/quality of the software really did play an important role is WhatsApp. I remember when there were a bunch of competing services, but WhatsApp was the only reliable one. As far as I can tell there was nothing else that WhatsApp did better, and yet they 'won' (at least in Holland/Europe).
> one example where I think the stability/quality of the software really did play an important role is WhatsApp
The interesting part is, WhatsApp is built using a dynamically-typed language whose guiding principle is to "let it crash." Your code will have bugs so plan accordingly.
as you say, the other thing is: what is “correct” today won’t necessarily be “correct” tomorrow
if it takes 2x or 3x to get to the next iteration then what’s the point... (again, assuming we aren’t talking pacemakers etc)
just my feeling, but these low level languages that try to have it both ways (working in the bit/byte realms, but also super high correctness) aren’t suitable for the realm of high iteration.... instead some high level language amenable to rapid iteration but still have high reliability should instead be built on top of something like rust but not necessarily _in_ it...
Yeah you're right, and it's almost certainly the chief constraint most software engineers labor under.
But this is a classic race to the bottom, and regulation is coming. The days when you could write an app that takes a person's information and stores it negligently are drawing to a close. Given sufficient liability penalties, the economic question will shift away from "what if we're late" to "what if it's broken", and that's when you'll start seeing a shift away from languages like C/C++ (and probably also languages like Python and JavaScript) towards languages/platforms/tooling that provide strong, indemnifying guarantees.
That would be also a great way for the large companies like Google (who can afford to take their time and pay fines when they need) to eliminate all smaller shops -- by extending those penalties in many places where it's not needed (eg. no personal data involved).
Like BS regulations in cheese, wine making etc, has eliminated small regional producers (once dominant) in favor of large conglomerates -- at least France is somewhat holding up.
Yeah it's kind of a quandary with regulations: larger organizations have the resources to comply with them while smaller ones don't. There are things you can do to work around it though (though admittedly they're rarely employed):
- Exempt smaller organizations. Maybe the classic example is the ACA in the US; if you're under a certain number of employees you don't need to provide health care. Obvious pitfalls, but still an option.
- Provide subsidies. This isn't exactly going to let a 10 person shop compete with someone like Airbus, but it does let you do things like hire staff and purchase tools to comply with regulations.
And separate from all that, it would be cool if we started enforcing antitrust legislation in the US again.
"Time to market" is what supposedly drives most technical debt, but most people would probably argue that our problem is having too much technical debt, not too little of it. And buggy code is a sort of tech debt that's especially costly to pay down - putting out fires in production is easily 10x as expensive as fixing the same issues at their outset via more careful coding.
I'm a beginner at rust, but I think this sentiment is correct. I'm finding developing in rust to be similar to the overhead of test-driven development. When I do TDD, I spend a lot more time getting to my MVP, at the benefit of catching a lot of bugs early and hopefully writing more correct code. Usually with TDD I'm pretty astonished at the code that I think is correct that fails very simple tests.
I have the assumption that once I am fluent in rust, more and more of the first code I write will be accepted by the borrow checker. The analogy is to C, where I don't really have to think consciously about, for example, assigning and dereferencing pointers. When I was a beginner C programmer (many years ago), I would write code and have it SIGSEGV immediately during test. Now that just doesn't happen unless I'm getting WAY too clever.
> How efficient is a developer when producing things that are incorrect? Unless the goal is produce incorrect things, which seems unlikely.
I have heard more than once that if we could spend a few hours less developing at the cost of having the product need to reboot every day or so, it was worth it. Of course it was no safety critical code, but in the end the only discriminant is money.
"How efficient is a developer when producing things that are incorrect?"
That software's users will use the product is the number one metric. They'll use it so long as it achieves their goal with the reliability or security they tolerate. That often means it can be kind of flaky in terms of reliability. The security can be arbitrarily bad so long as they don't know it. Sometimes they'll still use the product if they know security is bad because they need it.
That's the baseline. From there, developers have to decide what's most beneficial among investments in more features, enhancements of existing features, new products/activities, or enhancing quality/reliability/security. They usually choose against that last set. So, doing the other things with the minimum quality that's acceptable makes the most economic and social sense.
It's appealing to think there's a trade-off but in my experience there really isn't. I've been writing C++ and Rust for about the same length of time (4.5 years) and it at least feels to me like I am much better at shipping software when I write it in Rust: the work is done more quickly and I am more confident in its correctness.
Rust isn’t really the language you’d use to fool around for a one-use-script.
Although I must say that it replaced Python for most more complex programs for me. The type system makes it easier to read somebody elses code, even if they skipped all documentation.
Rust certainly forces good practice onto you. But on bigger projects good practice doesn’t reduce your productivity, but instead increases it, let alone to speak of the increased sustainability. Rust’s module system in combination with it’s type system and ownership rules leave very little dark spots for the programmer where weird things can happen, even when your project grows big. And if weird things happen they are a breeze to track down compared to python, usually. Rust sort of nudges you into the right choices, when you program Rust the Rust way.
If you are constantly fighting with the type system and the borrow checker that means you are probably still clinging to concepts you brought from other languages (at least it was like this for me). The moment I said: “Ok Rust, you won, from now on I will do it your way”, was the moment the compiler got my friend and things start to flow. Looking back I wonder why I ever thought I have to be able to force my abstractions into the code instead of taking a more data centric approach.
Is the productivity significantly lower than with python? Only if you are not firm with the language
Look up "design by contract" for more background on these.
I really hope this will be the next mainstream thing in programming language design, after the current functional wave. Even without fully perfected static analysis tools, just the dynamic checks alone are well worth the trouble of writing good contracts, IMO. They also make for better, more precise documentation.
Design by Contract (DbC) was seamlessly embedded into the Eiffel Language and Method right from the start, way back in 1986. The ideas gained by using Eiffel and Design by Contract can be formative and help us in our approach to using other languages.
The foundational ideas around DbC and Eiffel for requirements and their proof still evolve and progress 33 years later with AutoReq. A paper describing AutoReq was recently published ..
Code-level specifications (sometimes called contracts) that can be verified by various means (including manual deductive proofs, and automated solvers) exist for mainstream programming languages. The most mature ones are probably JML for Java (verified with https://www.openjml.org/ and various other tools) and ACSL for C (verified with https://frama-c.com/). C# has Spec#, but I'm not sure it's still used.
It is still unclear how best to use such code level verification, as the effort required grows very quickly with code size, and it's unclear how much sporadic verification of properties that are easy to prove actually improves correctness, but this is all still ongoing research.
Often it's best to just express preconditions in the normal types. For example, instead of having a `head-of-list` function that crashes with empty input, define its input to be of type `NonEmptyList`.
The power-to-weight ratio of refinement types is as unclear as that of contracts. You get more expressivity than simple types, but it's unclear whether it's enough to make a real impact. On the other hand, we're nowhere near being able to verify the properties that would make a real impact on code sizes that truly matter with automated proof techniques. Types are a bad fit for "deep" properties to begin with because they're tied to the proof theory of the type system. At least contracts have some leeway, as they can be verified more weakly but with much more scalable techniques (like randomized tests).
My biggest wish for Rust right now is dependent types, I find myself wanting them in almost everything I write to ensure it is correct for all possible inputs. It could also improve performance eliminating out of bounds checks in many places.
I recall someone mentioning in a RFC that it was on a distant wishful thinking roadmap. I hope it is.
Not very likely so far. Adding dependent types to the sort of uniqueness- and 'lifetime'/region-based typing that's used in Rust is very much a matter of research.
We had an RFC for Pi types [1] but in the ended, decided it was too much, too soon [2]. The "const generics" RFC [3] adds a minimal, forward-compatible from of this, and is on track to land this year.
You're right. I've spent too much time in GitLab, where they are counted separately :). And, besides, I forgot about the PRs to fix typos and so forth.
Is there anything you could do with dependant types that you can't do with a number of types wrapped in an enum? A dependently typed variable should have the same memory footprint of an enum, right? Do you just want a different syntax, or am I missing something?
With dependent types you can perform arithmetic at the type level. This lets you have functions that, e.g., take an array of length n and an array of length m and return an array of length n + m. Ideally, this would let you write programs that are provably correct with no runtime bounds checking.
I just read up on type arithmetic and I guess this is still whooshing over my head, because I can't see what this changes. I can have a function take two vectors of enums and return a new vector with the combined length. I can do operations based on the types of values held by variants in enums, matching only the possible variants. I don't see what can't be done as efficiently with an enum, but I'm very open to being ignorant and clueless.
If you have a function that returns the first n elements of a vector, how do you make sure there are enough elements? Most languages would either insert a runtime check or throw an exception at runtime. With a dependently typed language, you can do the check statically. This means knowing the provenance of n and the vector itself and doing a compile time proof that n can never exceed the length of the vector.
Okay, I see how that sort of check could be useful. I don't think it's impossible to do without dependant types in principle, but Rust isn't doing it AFAIK, and I see your point.
A classic example in Rust is to be generic over arrays. Arrays encode their length as part of the type; [T; N] is the type of an array of Ts that’s N elements long. In other words:
fn foo<T>(array: [T; ?]) {
How do you define ? to work on any length?
When the RFC I referenced above is implemented, you’d write
fn foo<T, const N>(array: [T; N]) {
and now you can call this function on arrays of varying lengths.
(In today’s Rust you’d use a slice instead, but that’s the simplest example I can give.)
Critical embedded systems for avionics and robotics systems frequently deal with values that must be within a certain range. Runtime bounds checking can be too expensive in these environments and dependent types would allow for provably correct bounded integers without checks. That is actually a problem I am dealing with right now in some MIL-STD-1553 data bus code.
While I was at NASA I was advocating for using Rust instead of C/C++ and FORTRAN and many people were interested because of the safety/performance aspects. I think it would take some serious ground from them in that area with dependent types also.
Just to elaborate a bit more, the use of optional values rather than NULL is really a special case dependent types. It's saying that no type can contain a non-value. For another example, imagine subtracting something from an unsigned int. You need to ensure that the value never goes below zero If you have an expression like 'x - 1', then the compiler needs to ensure that x is always > 0.
The nice thing about this kind of static analysis for critical systems is that there are often extreme consequences if a runtime check fails. What do we do for the nuclear power control system when we detect an error? Crash? Shut down the system? But the system is not functioning properly. How do we know that we can safely shut it down? These are pretty horrible things to consider. It's much better to be able to say analytically that the situation can not happen.
I once worked in a high energy physics lab, though. There is always memory corruption to contend with, so you'll never be free of runtime errors ;-)
In the space of safety-critical software systems with tight constraints, Ada has typically been the go-to language. Together with the verification sub-language, SPARK, it can prove things like array bounds (and I assume integer bounds) are respected, without runtime checks. See e.g. https://www.adacore.com/gems/gem-68
The formal verification method used by SPARK is industry-proven (for decades). Dependent types are for the most part still an academic curiosity struggling to find industrial application. Of course they may very well do that, one day. But today, if you're working on safety-critical systems, I hope you take a close look at Ada+SPARK.
The Stanford Pascal Verifier was probably the first[1] The Pascal-F Verifier, a project I headed around 1980,[2][3] used preconditions and postconditions very similar to what this guy is doing in Rust. "Specifically, full functional correctness with properties like arithmetic correctness, in-bounds array accesses, state machines correctness, functional correctness with respect to an abstract specification or security properties." - we had all that in 1983. Look at the example starting at page 56 in [2].
DEC did a lot of work on this for Modula, and later Java, in the late 1980s.[4] Modula went down with DEC. The work was mostly lost. Dafny is probably the most modern system in this line.
Memory safety by proof was coming along well in the early 1980s. Working systems existed. Automatic prover technology was working. Then came C.
The "array is a pointer" mindset of C set programming back by decades. In Pascal, there were no buffer overflows. Pascal, Modula, Ada, and on to Rust - no buffer overflows. Everything carried along size information. Subscript checking optimizations had been figured out by the 1980s, so the performance penalty was coming down.
The author mentions Sapiens, an attempt to apply machine learning to the problem of null pointers in C. (Anyone have a reference? It's hard to find.) Massive amounts of effort are being applied to try to infer information that C just can't express. This would be a lot more worthwhile if it resulted in translation of C to something better.
Formal methods and "proving" "correctness" have not taken off because while they seem like a great idea, it's insanely expensive to do it for non-trivial software, and you end up with a provably correct piece of software that is still full of business logic bugs and which inevitably fails to keep up with ever-changing business processes.
I agree that software is terrible, and programming language choice plays a big role in what sorts of mistakes you can make, but I'm skeptical that attempting to write provably correct programs is a remotely realistic goal. Sure, it's possible to prove an algorithm, but the real world software systems that need the help--certainly anything that involves more than one process on a single CPU--have complexity that goes well beyond what can be modeled or reasoned about, much less be proven.
It's not that hard to automatically prove that a large piece of software has no buffer overflows and no null pointer dereferences. We had that working decades ago.
If this has solved the issue of automatically proving that any C or C++ program has no buffer overflows, why do we still see CVEs for popular libraries and software that result from them?
The tools can also miss things. They miss more as complexity goes up. High-assurance systems used to structure things in a hierarchical way with simple functions and only call downs to aid the analysis. Basically, reduce combinatorial explosion. Most software isn't structured anything like that. It does combinatorial explosion with C not giving analyzer a lot of information to begin with. So, it causes tools to miss things.
Rust might be easier to analyze due to the type system. Those labels become inputs and heuristics for future static analyzers.
Because people can't resist chasing proven incorrect code ("find bugs"), instead of overhauling programs for proven correct code. Because the latter is a lot of work.
How does this deal with higher-order functions? This is usually where these analyzers fall down. If you don't allow higher-order functions, then you just forbade virtual methods, so your analyzer can't handle real-world C/C++ code.
Off-hand, I don't know how it handles higher-order functions. It analyzes LLVM IR, not the source directly, so I guess it depends on how virtual methods are represented in LLVM IR and whether those instructions are supported or ignored by the tool.
The tool doesn't claim to handle everything, and doesn't claim to be complete. You can absolutely write code that it can't analyze because it's either too complicated or you're using unsupported language features. If you want your code to be analyzable, then you have to write it that way. The tool isn't magic.
Don't you think it's an over-statement to say that it can't handle real-world code if it doesn't support higher-order functions? Not all C++ code uses virtual methods, and C doesn't even have this feature in the language.
It's really not that hard, but it's important to remember that while these tools do guarantee no undefined behavior, they may require either adding annotations or changing the program a bit. Their goal is to guarantee lack of UB not for free, but at a cost that's drastically lower than a rewrite in a safe language, something they deliver on quite well.
So, for example, suppose you have a higher order function that takes a function returning a pointer, calls it, and dereferences its return value. For simplicity, let's assume we only care about NULL dereferencing and not other kinds of invalid memory, but the idea is the same. You then have two options: either you annotate the argument to require that it cannot return NULL -- in which case the tool would attempt to prove that any function passed as an argument satisfies this (possibly with the help of further annotations) -- or you add a runtime check, in which case the automatic proof is simple.
No false negative sounds nice, but the problem is the amount of false positives. The Unix `true` command is also a static analyser with no false negative (but 100% false positive on perfect code).
And a perfect static analyser with no false negative or false positive is equivalent to solving the halting problem. So what we need is a «good enough» solution working with existing code. But the amount of CVEs and the low adoption of such tools empirically shows that we are far from there.
Ada may vaguely resemble Lua but aerospace grade code (think SPARK) is about as fun to write as assembly. Rust is not perfect but it has momentum and tons of free tooling. At this point it would be easier to just try to add more safety features to Rust than push for the adoption of a language without the conveniences expected of a post-Y2K programming language.
There's a engineering-oriented middle ground that doesn't prove everything mathematically from first principles like Coq. Languages like Ada and Haskell can get you a long way without formal proofs.
It's hard because most languages do not help with that. There's not an easy option to get all the potential unhandled error sites for a code base. Even in Rust you can sprinkle your code full of "?" and you transformed back into runtime errors. Which is okay, if you understand it. It'd be great if such programming decisions could be annotated, then when someone imports a library it'd be easy to get a human readable list of potential runtime errors (edge cases).
But usually when it's time to just churn out yet another app, cost-benefit analysis indicates that fuck that, let's use pokemon error handling.
And it's hard to blame anyone for such a decision when the alternative is going a few more days without the shiny new app/feature. The end of the financial quarter is coming. The app/feature must "work".
And that's why it's not surprising that no one uses Coq and Idris for run of the mill business as usual apps.
? doesn't transform anything back into a runtime error. It's explicitly saying "I don't know how to handle any errors that happen here, so give it back to the caller." The "potential unhandled errors" are all still perfectly listed inside the return type.
Uh, thanks! You are completely right. I forgot that it's not just an unconditional unwrap.
What I wanted to communicate is that I find that in many cases error handling is a sort of twilight zone. When the environment or context of the running program is not what it should be. (Eg file not found, lack of permission to write to it, not enough memory, something is not configured, missing runtime dependency; and all the state validation errors, etc.) And the errors that result from this are usually too low level, and there is rarely enough information in the error messages (types) themselves to help understand (and potentially work around) the condition causing the error.
Proving correctness is always an incremental win when executed correctly. Everything that can be proved correct is one more bug that your editor will underline in red, and often one less test to be written.
Agreed. Ada 2012 [1] and Spark [2] (an Ada subset with formal verification features) provide production-ready versions of most of these features.
Clojure's spec [3] is also promising for better specifications and more automated testing
Over the past decade or so, we have seen many mainstream programming languages adopt functional programming features. My hope is that more mainstream languages adopt preconditions, postconditions, invariants, and useful formal verification features. There are so many more great tools that could be used to build high quality software than unit testing.
The Coders At Work interview with Fran Allen really hammered home that point. Which begs the question, why did C get so popular? I guess what programmers like to use isn't really what is always best for them. People like to ride motorcycles and programmers like to use C.
Some people would say that C got popular (apart from the obvious UNIX sponsorship) because at its core it is just a fancy way to address memory like in assembly, but almost portable.
Because, C is portable assembler. In Pascal, for example, if something cannot be done in Pascal, then assembler must be used. If assembler is used, then program is tied to single platform. If you need to support two or more platforms at same time over long period, then C wins.
That is the myth, in practice ISO C specifies an abstract machine and libc is impossible to be written 100% in ISO C, some functions require either external Assembly or language extensions for their implementation.
Naturally Modula-2 also faces the same issue. What it offers is better type safety and being honest about it.
The whole point is that contrary to its sales prospect, not only does C also require to write Assembly, it doesn't have any language support for modern hardware CPU/GPUs, just like any other high level language, requiring extensions to the standard, not necessarly portable across implementations.
Too many years are passed, but as far as I remember, only C code was portable between 8, 16, and 32 bit platforms. It was possible to incrementally convert program from assembler to C and then port to different platforms, but it was not possible to do conversion using Pascal, or other programming language.
Yeah, if you were writing using a safe subset across all C variants that happened to be supported across all those C compilers.
Check language support across Small-C, Turbo C, Quick C, Aztech C, Metrowerks C and many others from those days.
Likewise it was possible to do the same across Pascal compilers that implemented variants of ISO Extended Pascal/UCSD Pascal, Modula-2 and a couple of other high level languages.
That capability is shared among all high level programming languages, nothing special about C here, once upon a time it was also only available to UNIX users.
That's because the C++ compiler has no idea what you're doing. It can't hoist subscript checks out of loops, because it doesn't know they're subscript checks. They're something some template generated, and at bottom, they expand to an IF statement. The Go compiler, which knows about subscript checks, does some of those optimizations.
For this optimization to work, the compiler has to be allowed to report subscript errors early. Frequent subscript checks that cause noticeable overhead tend to be inside loops. Often, the compiler could hoist the implicit assert inside the loop up to one assert checked before the loop is entered. It has to be allowed to report failure as soon as it become inevitable. If you have a loop from 0 to 100 over an array that's 0 to 99, and there's no way to exit the loop early, then failure is inevitable.
As soon as failure is inevitable, it has to be OK to detect it. That means if you're printing values 0 to 100, you'll never even get the first one printed. You'll abort before entering the loop. This is a bit strange to C/C++ programmers.
Once the assert has been hoisted out of the loop, the compiler may be able to prove that it can't fail. For FOR statements, this is usually easy. So the subscript checking overhead can completely disappear for many inner loops.
> As soon as failure is inevitable, it has to be OK to detect it. That means if you're printing values 0 to 100, you'll never even get the first one printed. You'll abort before entering the loop. This is a bit strange to C/C++ programmers.
It's strange but compilers are allowed to do it and anyone sufficiently familiar with undefined behavior will not be surprised.
Ah, so the compiler doesn't understand it's a failure, and just sees normal program flow that it can't alter.
That's a tricky thing to solve, yeah. At best, under current semantics, the compiler could emit a fast loop and a slow loop, and pick which one using an initial bounds check. But that's extremely awkward at best...
Automatically handling the bounds check upfront is a type of control flow that's halfway between normal exceptions and undefined behavior, that C++ doesn't really grok.
When I dabbled in gfortran, a feature I liked was that while no bounds-checking is the default, run time bounds-checks can be enabled with "-fcheck=bounds" or "-fcheck=all", which can be handy while developing/testing code.
Alternatively, Julia has a macro "@inbounds" which disables checks, but this involves going through and annotating code after testing. You can also start Julia with the options "--check-bounds={yes|no}" to override declarations.
Running testsuites enables all checks.
Seems like it would be handy if these checks could be elided by defining a macro. Any reason this isn't done?
The performance cost is often much higher than the time spent repeatedly checking bounds. It tends to defeat the auto-vectorizer.
Another workaround is to manually check bounds before the loop. This lets the compiler prove all bounds checks pass if it gets to the loop, and solves the problem.
I do wish that sort of thing could be automatic.
If that's the semantics you want, why not just add a check at the beginning of the loop? Compilers could add a warning advising the developer to do this if she doesn't care about partial results, anytime that they can't fully eliminate an .at() bounds check inside a loop.
It's a matter of economics, mostly: proving that a feature is mathematically correct costs a lot more than implementing the feature itself, and so mathematic proofs are not done except if the cost justifies it.
And because of that the tools that do these proofs do not take off, and thus they get reinvented every few years with each programming language.
Raw pointers exist. Unsafe Rust exists. Any large enough Rust project will
end up with some unsafe code. That doesn't mean that the things OP is doing
aren't great—they are—but merely that, when considering tools to be used
for real-world Rust, people shouldn't assume that their tools will only be
used in a shiny rainbow unicorn world of Safe Rust.
Looking at examples of syntax for pre/post-conditions and invariants, it's all Rust expressions inside strings. Is there no other way for an attribute to have some associated inline code? Strings are not optimal for this, because they break tooling (syntax highlighting, code completion and navigation, refactoring etc).
From tooling perspective, this isn't perfect, because there's still no guarantee that the token stream is a valid expression. So e.g. an IDE trying to highlight them or do a global rename refactor has to assume, which might not always be correct for token-based DSLs. It would be nice to have some metadata to distinguish those. Or perhaps there is an idiomatic way to express it in a contract on the macro itself, that tools could look at?
I'm surprised there is no name dropping of `Hoare logic' here or in the article so i'm gonna do it. Hoare logic is made of triplets (precondition, command, postcondition). A whole bunch of things are based on that. To go further one can also search about separation logic which adds an account for abstract memory locations into hoare logic.
But actually i must say i'm not very fond of these kind of approaches. As is rightly made explicit in the post, a lot of nice properties of Rust come from it's type system. A type system is a way to annotate usual programming constructs with additional infos (types) together with a decidable procedure for testing whether or not a particular program is well-typed. And then we provide several key lemmas asserting that all well-typed program enjoy such and such property. On the other hand, program verification is a different beast: you annotate parts of your program with some form of specification (hoare triplets and the like) and then you try to solve the (in most case undecidable) problem of coming up with proofs that your program satisfies the specifications you gave.
The approach is very different: on one hand you restrict (maybe severely) the programs so that you can decide whether or not some properties hold, on the other hand you (mostly) don't restrict the programs and you hope to give enough hints so that the solver doesn't get stuck. Bottom-up versus top-down. Correct-by-construction versus maybe-provably-correct. I feel like type checking is robust/reliable/simple whereas verification is a black-box which isn't easy to understand and thus never feels very "principled". Sure types can sometimes be too explicit and heavy on the user, but they are also more predictable and consistent.
My 2cts... Anyway i'm not saying i think this project is useless or anything, most systems actually live somewhere between bottom-up and top-down, ideas from one side may help the other, and deductive verification may arguably be much more bottom-up than other verification techniques (all flavors of model checking, abstract interpretation etc).
Deductive verification is a large extension of designing by contract: The addition of a SMT solver to verify the contracts at compile time for instance. On the other hand libhoare only adds the contracts as a runtime addition with no mention of formally verifying these.
The same with the RFC, it dismissed automatic verification: "Automated proof systems are very hard, especially when AFAIK Rust's type system doesn't even have partial formal proofs yet."
This paper shows a similar approach to OP's but applied to Curry: https://arxiv.org/abs/1709.04816. It shows how no formal proofs are needed. However Curry is significantly more pure.
132 comments
[ 3.9 ms ] story [ 133 ms ] threadhttps://github.com/servo/servo/pull/22458
https://github.com/denismerigoux/rox-star/blob/master/textin...
For instance, the `is_diagonal` function provided as the "correctness checker" looks to me like something that would be in a unit test for the `double` function. However, I think it goes a little bit deeper than that. In a unit test, you are somewhat required to pass specific values to the constructs you are testing. The given example is more complete than a unit test in that it doesn't just test for the correct value being produced by the `double` function when given specific values, it actually checks all possible outcomes by asserting that the `double` function always produces a `Point` where `p.x == p.y`.
Given that the example is relatively trivial, I would like to see how this would work for more complex functions and structures.
[1] https://www.scalacheck.org/
[0] https://blog.merigoux.ovh/en/2019/04/16/textinput.html
Maybe you know this, but this is a well known correspondence (as in academically from decades ago, but barely mentioned in industry): https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
The types you write in code describe program properties to be proven and the type checker tries to create a proof that those properties are true for all inputs and outputs. Tests as you say only check a small number of inputs/outputs in comparison. It's very similar to mathematics where checking if a conjecture holds for a few values is a poor substitute to a rigorous proof.
Yes, it does look impenetrable but the high-level idea is fairly intuitive and it's the foundation of many formal proof assistants (e.g. Coq, Idris).
I see comments quite often where people suspect some vague links between writing maths proofs and type checking computer programs so I think it's worth knowing a very deep connection has been known about this and researched for decades.
[0]: https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%...
I wouldn't say using a "unit test" is ever really a viable option for me. Property-based tests subsume unit tests.
So no, Coq and other "total" programing languages (agda, idris, F*) may not be turing complete in the usual sense because the two things are contradictory, but they are much better: you can simulate a turing machine as a server which will be provably always making progress in finite time.
See this paper for some more insights:
https://personal.cis.strath.ac.uk/conor.mcbride/TotallyFree....
(Contrast with long compile times which are incompressible)
[1] https://clojure.org/guides/spec
It seems like the philosophy prefers knowing ahead of time what's wrong over discovering it incidentally, and probably accidentally, after the fact.
I discovered a bug that could potentially be triggered in the codebase where I work, but never has. It's about 5 years old.
You don't actually always need technically correct - sometimes you want practically correct, where "practically" covers a huge spectrum.
Because if say, 75% of your time is spent debugging in an "regular" language then you really aren't saving much time by reducing the amount of code you must write.
If we could reduce programming to typing in mostly correct code then software development will be much faster, even if the code we type is 50% longer.
Of course everyone wants the best of both worlds: everything now, zero bugs. Fast, cheap, right: pick two applies despite everyone wanting all three.
I thought we were discussing the trade-offs of typing a little more to guarantee correctness, or at least eliminate a class of software errors.
You're doing that Appeal to the Extremes Fallacy:
https://www.logicallyfallacious.com/tools/lp/Bo/LogicalFalla...
I'm not falling into appeal to extreme, even though I did point out an extreme.
I'll disagree with this one. Refactoring old and rarely-touched code is bliss when working under a strong type system, at least relative to dynamic or weakly-typed languages. The key to the timely resolution of technical debt is to allow things to be updated in piecemeal rather than in one enormous burst; this requires solid abstraction boundaries and encapsulation, both of which are provided by types (in addition to other features of a language, such as a module system). The fact that Rust so heavily discourages global state is another point in its favor.
We can agree that there are contexts where correctness is less important than velocity, e.g. prototyping, though languages that front-load correctness at the expense of velocity are going to produce less technical debt in the first place, because the debts can be paid off before they accrue interest.
That said, it’s not that simple. There are threshold effects (more than X amount of time = your company is dead) and intangibles (how do you feel while programming).
But anyone making a blanket statement without considering these things is participating in a dumb internet argument.
How is this confusing?
If it takes you 2 weeks with language X to write a sloppily written app, that works 99% of the time but has some errors -- and 2 months with Rust to write a version of the same app that has no errors, what you'd you prefer?
Ever heard of "time to market"? What good it would be if you get it 100% right, and your competitor has their app already out, and captured all your potential customers?
And even if time to market is not involved, would you really care for some occasional errors, if you get the majority of the functionality you want working just fine?
If you build pacemakers and airplanes, the answer is yes.
If you build regular websites, apps, and scripts, the answer might very well be no.
That's the case, just the numbers (2 weeks, 100% etc) are made up.
It’s a large, multi-variable problem. This is why it’s great that we have so many languages!
A constant stream of bugs have driven customers away before too, so if you're waiting in the wings with a bug-free/verified version of your competitor's program, you have a real shot at stealing their customers. First mover advantage is important, but so is quality if marketed properly.
I admit personally I'm inclined to agree with coldtea. But one example where I think the stability/quality of the software really did play an important role is WhatsApp. I remember when there were a bunch of competing services, but WhatsApp was the only reliable one. As far as I can tell there was nothing else that WhatsApp did better, and yet they 'won' (at least in Holland/Europe).
Microsoft had a features-first mindset, which led to a Swiss-cheese-manifold of bugs and security flaws.
The result was that you couldn't install anything without risking a virus.
Businesses went with browser based solutions to avoid that risk.
The interesting part is, WhatsApp is built using a dynamically-typed language whose guiding principle is to "let it crash." Your code will have bugs so plan accordingly.
if it takes 2x or 3x to get to the next iteration then what’s the point... (again, assuming we aren’t talking pacemakers etc)
just my feeling, but these low level languages that try to have it both ways (working in the bit/byte realms, but also super high correctness) aren’t suitable for the realm of high iteration.... instead some high level language amenable to rapid iteration but still have high reliability should instead be built on top of something like rust but not necessarily _in_ it...
[edit] forgot to mention parent post
But this is a classic race to the bottom, and regulation is coming. The days when you could write an app that takes a person's information and stores it negligently are drawing to a close. Given sufficient liability penalties, the economic question will shift away from "what if we're late" to "what if it's broken", and that's when you'll start seeing a shift away from languages like C/C++ (and probably also languages like Python and JavaScript) towards languages/platforms/tooling that provide strong, indemnifying guarantees.
Like BS regulations in cheese, wine making etc, has eliminated small regional producers (once dominant) in favor of large conglomerates -- at least France is somewhat holding up.
- Exempt smaller organizations. Maybe the classic example is the ACA in the US; if you're under a certain number of employees you don't need to provide health care. Obvious pitfalls, but still an option.
- Provide subsidies. This isn't exactly going to let a 10 person shop compete with someone like Airbus, but it does let you do things like hire staff and purchase tools to comply with regulations.
And separate from all that, it would be cool if we started enforcing antitrust legislation in the US again.
I have the assumption that once I am fluent in rust, more and more of the first code I write will be accepted by the borrow checker. The analogy is to C, where I don't really have to think consciously about, for example, assigning and dereferencing pointers. When I was a beginner C programmer (many years ago), I would write code and have it SIGSEGV immediately during test. Now that just doesn't happen unless I'm getting WAY too clever.
I have heard more than once that if we could spend a few hours less developing at the cost of having the product need to reboot every day or so, it was worth it. Of course it was no safety critical code, but in the end the only discriminant is money.
That software's users will use the product is the number one metric. They'll use it so long as it achieves their goal with the reliability or security they tolerate. That often means it can be kind of flaky in terms of reliability. The security can be arbitrarily bad so long as they don't know it. Sometimes they'll still use the product if they know security is bad because they need it.
That's the baseline. From there, developers have to decide what's most beneficial among investments in more features, enhancements of existing features, new products/activities, or enhancing quality/reliability/security. They usually choose against that last set. So, doing the other things with the minimum quality that's acceptable makes the most economic and social sense.
Although I must say that it replaced Python for most more complex programs for me. The type system makes it easier to read somebody elses code, even if they skipped all documentation.
Rust certainly forces good practice onto you. But on bigger projects good practice doesn’t reduce your productivity, but instead increases it, let alone to speak of the increased sustainability. Rust’s module system in combination with it’s type system and ownership rules leave very little dark spots for the programmer where weird things can happen, even when your project grows big. And if weird things happen they are a breeze to track down compared to python, usually. Rust sort of nudges you into the right choices, when you program Rust the Rust way.
If you are constantly fighting with the type system and the borrow checker that means you are probably still clinging to concepts you brought from other languages (at least it was like this for me). The moment I said: “Ok Rust, you won, from now on I will do it your way”, was the moment the compiler got my friend and things start to flow. Looking back I wonder why I ever thought I have to be able to force my abstractions into the code instead of taking a more data centric approach.
Is the productivity significantly lower than with python? Only if you are not firm with the language
I really hope this will be the next mainstream thing in programming language design, after the current functional wave. Even without fully perfected static analysis tools, just the dynamic checks alone are well worth the trouble of writing good contracts, IMO. They also make for better, more precise documentation.
The foundational ideas around DbC and Eiffel for requirements and their proof still evolve and progress 33 years later with AutoReq. A paper describing AutoReq was recently published ..
AutoReq: Expressing and verifying requirements for control systems https://www.sciencedirect.com/science/article/pii/S1045926X1...
It is still unclear how best to use such code level verification, as the effort required grows very quickly with code size, and it's unclear how much sporadic verification of properties that are easy to prove actually improves correctness, but this is all still ongoing research.
Refinement types are also worth exploring in this space, as they appear to give a good power-to-weight. See Liquid Haskell, for example, https://ucsd-progsys.github.io/liquidhaskell-tutorial/03-bas...
I recall someone mentioning in a RFC that it was on a distant wishful thinking roadmap. I hope it is.
1: https://github.com/rust-lang/rfcs/issues/1930
2: https://github.com/rust-lang/rfcs/pull/1657#issuecomment-268... and https://github.com/rust-lang/rfcs/pull/1931#issuecomment-304...
3: https://github.com/rust-lang/rfcs/blob/master/text/2000-cons...
We may or may not end up with them someday, but we need experience with RFC 2000 first.
When the RFC I referenced above is implemented, you’d write
and now you can call this function on arrays of varying lengths.(In today’s Rust you’d use a slice instead, but that’s the simplest example I can give.)
While I was at NASA I was advocating for using Rust instead of C/C++ and FORTRAN and many people were interested because of the safety/performance aspects. I think it would take some serious ground from them in that area with dependent types also.
The nice thing about this kind of static analysis for critical systems is that there are often extreme consequences if a runtime check fails. What do we do for the nuclear power control system when we detect an error? Crash? Shut down the system? But the system is not functioning properly. How do we know that we can safely shut it down? These are pretty horrible things to consider. It's much better to be able to say analytically that the situation can not happen.
I once worked in a high energy physics lab, though. There is always memory corruption to contend with, so you'll never be free of runtime errors ;-)
The formal verification method used by SPARK is industry-proven (for decades). Dependent types are for the most part still an academic curiosity struggling to find industrial application. Of course they may very well do that, one day. But today, if you're working on safety-critical systems, I hope you take a close look at Ada+SPARK.
The Stanford Pascal Verifier was probably the first[1] The Pascal-F Verifier, a project I headed around 1980,[2][3] used preconditions and postconditions very similar to what this guy is doing in Rust. "Specifically, full functional correctness with properties like arithmetic correctness, in-bounds array accesses, state machines correctness, functional correctness with respect to an abstract specification or security properties." - we had all that in 1983. Look at the example starting at page 56 in [2].
DEC did a lot of work on this for Modula, and later Java, in the late 1980s.[4] Modula went down with DEC. The work was mostly lost. Dafny is probably the most modern system in this line.
Memory safety by proof was coming along well in the early 1980s. Working systems existed. Automatic prover technology was working. Then came C.
The "array is a pointer" mindset of C set programming back by decades. In Pascal, there were no buffer overflows. Pascal, Modula, Ada, and on to Rust - no buffer overflows. Everything carried along size information. Subscript checking optimizations had been figured out by the 1980s, so the performance penalty was coming down.
The author mentions Sapiens, an attempt to apply machine learning to the problem of null pointers in C. (Anyone have a reference? It's hard to find.) Massive amounts of effort are being applied to try to infer information that C just can't express. This would be a lot more worthwhile if it resulted in translation of C to something better.
Forty years, and this still isn't fixed.
[1] http://i.stanford.edu/pub/cstr/reports/cs/tr/79/731/CS-TR-79... [2] http://www.animats.com/papers/verifier/verifiermanual.pdf [3] https://github.com/John-Nagle/pasv [4] https://link.springer.com/content/pdf/10.1007/BFb0026441.pdf
I agree that software is terrible, and programming language choice plays a big role in what sorts of mistakes you can make, but I'm skeptical that attempting to write provably correct programs is a remotely realistic goal. Sure, it's possible to prove an algorithm, but the real world software systems that need the help--certainly anything that involves more than one process on a single CPU--have complexity that goes well beyond what can be modeled or reasoned about, much less be proven.
Unless the code is in C. Then it's really hard.
[1] https://github.com/NASA-SW-VnV/ikos/blob/master/analyzer/REA...
http://www.ganssle.com/tem/tem372.html#article4
The tools can also miss things. They miss more as complexity goes up. High-assurance systems used to structure things in a hierarchical way with simple functions and only call downs to aid the analysis. Basically, reduce combinatorial explosion. Most software isn't structured anything like that. It does combinatorial explosion with C not giving analyzer a lot of information to begin with. So, it causes tools to miss things.
Rust might be easier to analyze due to the type system. Those labels become inputs and heuristics for future static analyzers.
The tool doesn't claim to handle everything, and doesn't claim to be complete. You can absolutely write code that it can't analyze because it's either too complicated or you're using unsupported language features. If you want your code to be analyzable, then you have to write it that way. The tool isn't magic.
Don't you think it's an over-statement to say that it can't handle real-world code if it doesn't support higher-order functions? Not all C++ code uses virtual methods, and C doesn't even have this feature in the language.
So, for example, suppose you have a higher order function that takes a function returning a pointer, calls it, and dereferences its return value. For simplicity, let's assume we only care about NULL dereferencing and not other kinds of invalid memory, but the idea is the same. You then have two options: either you annotate the argument to require that it cannot return NULL -- in which case the tool would attempt to prove that any function passed as an argument satisfies this (possibly with the help of further annotations) -- or you add a runtime check, in which case the automatic proof is simple.
And a perfect static analyser with no false negative or false positive is equivalent to solving the halting problem. So what we need is a «good enough» solution working with existing code. But the amount of CVEs and the low adoption of such tools empirically shows that we are far from there.
But usually when it's time to just churn out yet another app, cost-benefit analysis indicates that fuck that, let's use pokemon error handling.
And it's hard to blame anyone for such a decision when the alternative is going a few more days without the shiny new app/feature. The end of the financial quarter is coming. The app/feature must "work".
And that's why it's not surprising that no one uses Coq and Idris for run of the mill business as usual apps.
What I wanted to communicate is that I find that in many cases error handling is a sort of twilight zone. When the environment or context of the running program is not what it should be. (Eg file not found, lack of permission to write to it, not enough memory, something is not configured, missing runtime dependency; and all the state validation errors, etc.) And the errors that result from this are usually too low level, and there is rarely enough information in the error messages (types) themselves to help understand (and potentially work around) the condition causing the error.
Clojure's spec [3] is also promising for better specifications and more automated testing
Over the past decade or so, we have seen many mainstream programming languages adopt functional programming features. My hope is that more mainstream languages adopt preconditions, postconditions, invariants, and useful formal verification features. There are so many more great tools that could be used to build high quality software than unit testing.
[1] https://www.ada2012.org/
[2] https://en.wikipedia.org/wiki/SPARK_(programming_language)
[3] https://clojure.org/about/spec
https://github.com/rust-lang-nursery/wg-verification/issues/...
It's good to see that Rust is learning from Ada. Ada is also learning from Rust: https://arxiv.org/abs/1710.07047
K&R was published in 1978. So at best this story and timeline are incomplete.
More illuminating would be an account of why C beat these other languages in the marketplace in the 80s, despite its disadvantages in safety.
Had Bell Labs been allowed to sell UNIX at the same price as other companies were selling theirs, and C would never have taken off.
Burroughs, developed in 1961 in a memory safe systems programming language is still sold by Unisys as ClearPath MCP.
Same applies to the IBM mainframes.
The surviving systems from the 60-70's where C only plays a guest role at most.
The whole point is that contrary to its sales prospect, not only does C also require to write Assembly, it doesn't have any language support for modern hardware CPU/GPUs, just like any other high level language, requiring extensions to the standard, not necessarly portable across implementations.
Check language support across Small-C, Turbo C, Quick C, Aztech C, Metrowerks C and many others from those days.
Likewise it was possible to do the same across Pascal compilers that implemented variants of ISO Extended Pascal/UCSD Pascal, Modula-2 and a couple of other high level languages.
well, we're in 2019 and replacing a few critical .at() by [] regularly allows me to gain a few % when benchmarking.
For this optimization to work, the compiler has to be allowed to report subscript errors early. Frequent subscript checks that cause noticeable overhead tend to be inside loops. Often, the compiler could hoist the implicit assert inside the loop up to one assert checked before the loop is entered. It has to be allowed to report failure as soon as it become inevitable. If you have a loop from 0 to 100 over an array that's 0 to 99, and there's no way to exit the loop early, then failure is inevitable.
As soon as failure is inevitable, it has to be OK to detect it. That means if you're printing values 0 to 100, you'll never even get the first one printed. You'll abort before entering the loop. This is a bit strange to C/C++ programmers.
Once the assert has been hoisted out of the loop, the compiler may be able to prove that it can't fail. For FOR statements, this is usually easy. So the subscript checking overhead can completely disappear for many inner loops.
I have seen plenty of code like that, specially when written by the occasional C++ coder that usually works in other languages.
It's strange but compilers are allowed to do it and anyone sufficiently familiar with undefined behavior will not be surprised.
That's a tricky thing to solve, yeah. At best, under current semantics, the compiler could emit a fast loop and a slow loop, and pick which one using an initial bounds check. But that's extremely awkward at best...
Automatically handling the bounds check upfront is a type of control flow that's halfway between normal exceptions and undefined behavior, that C++ doesn't really grok.
Alternatively, Julia has a macro "@inbounds" which disables checks, but this involves going through and annotating code after testing. You can also start Julia with the options "--check-bounds={yes|no}" to override declarations. Running testsuites enables all checks.
Seems like it would be handy if these checks could be elided by defining a macro. Any reason this isn't done?
The performance cost is often much higher than the time spent repeatedly checking bounds. It tends to defeat the auto-vectorizer.
Another workaround is to manually check bounds before the loop. This lets the compiler prove all bounds checks pass if it gets to the loop, and solves the problem. I do wish that sort of thing could be automatic.
And because of that the tools that do these proofs do not take off, and thus they get reinvented every few years with each programming language.
"I do not intend to tackle the difficult problem of interaction between unsafe and safe Rust code; Rustbelt is the correct way to do it."
The statement you quoted is clearly in the implied context of safe code.
Clearly you don't.
https://blog.rust-lang.org/2019/04/11/Rust-1.34.0.html#custo...
From tooling perspective, this isn't perfect, because there's still no guarantee that the token stream is a valid expression. So e.g. an IDE trying to highlight them or do a global rename refactor has to assume, which might not always be correct for token-based DSLs. It would be nice to have some metadata to distinguish those. Or perhaps there is an idiomatic way to express it in a contract on the macro itself, that tools could look at?
But actually i must say i'm not very fond of these kind of approaches. As is rightly made explicit in the post, a lot of nice properties of Rust come from it's type system. A type system is a way to annotate usual programming constructs with additional infos (types) together with a decidable procedure for testing whether or not a particular program is well-typed. And then we provide several key lemmas asserting that all well-typed program enjoy such and such property. On the other hand, program verification is a different beast: you annotate parts of your program with some form of specification (hoare triplets and the like) and then you try to solve the (in most case undecidable) problem of coming up with proofs that your program satisfies the specifications you gave.
The approach is very different: on one hand you restrict (maybe severely) the programs so that you can decide whether or not some properties hold, on the other hand you (mostly) don't restrict the programs and you hope to give enough hints so that the solver doesn't get stuck. Bottom-up versus top-down. Correct-by-construction versus maybe-provably-correct. I feel like type checking is robust/reliable/simple whereas verification is a black-box which isn't easy to understand and thus never feels very "principled". Sure types can sometimes be too explicit and heavy on the user, but they are also more predictable and consistent.
My 2cts... Anyway i'm not saying i think this project is useless or anything, most systems actually live somewhere between bottom-up and top-down, ideas from one side may help the other, and deductive verification may arguably be much more bottom-up than other verification techniques (all flavors of model checking, abstract interpretation etc).
They call it "design by contract" rather than "deductive verification" though.
Wish there wouldn't be so many terms for the same thing.
edit: There's also an existing RFC for this: https://github.com/rust-lang/rfcs/issues/1077
The same with the RFC, it dismissed automatic verification: "Automated proof systems are very hard, especially when AFAIK Rust's type system doesn't even have partial formal proofs yet."
This paper shows a similar approach to OP's but applied to Curry: https://arxiv.org/abs/1709.04816. It shows how no formal proofs are needed. However Curry is significantly more pure.