Welcome to the research field of program refinement. There are a couple of approaches one can take:
- Certify: the program isn't actually checked/proven to satisfy the spec, but experts in the field will pore over the code and try to find any disparities or edge cases.
- Top-down: given a spec, try to generate an implementation that satisfies it by construction. This depends a lot of the concrete framework, but e.g. Coq supports extraction of executable code from its (verified) source. The results are not very well decoupled from the spec and are often lacking in performance (single-threaded, unoptimised, etc).
- Bottom-up: given an actual implementation, prove that it behaves according to the spec. This can allow for optimised programs and concurrency, but both complicate the proofs. (This happens to be my PhD research topic.)
Some work to look at, if you are curious: Event-B, Trillium, IronFleet
That's not inherent to PHP, but rather the ecosystem it's usually used in. The standard "LAMP" stack, for example, has Apache in it for the actual server, talking to PHP using a CGI interface. So if your PHP script crashes or hangs, the server itself is still up, and capable of serving other clients.
If you set up a Node script where e.g. Express talks directly to the clients, then yes, the script crashing or hanging means the server becomes unavailable or unresponsive. However, you can also set up a layer in front of Node. See cgi-node for replicating the CGI workflow you might be used to.
There are some advantages to the standard Node model though: the program can manage its own resources, such as keeping a database connection open; it can run asynchronous maintenance tasks; it can see and report the current server load; it can easily combine HTTP(S) communication and Web socket streams; etc.
Maybe you are thinking of zahada? It is as you describe, individual HTML pages solved by typing the correct answer into the address bar. It involved a lot of lateral thinking. Sometimes a bit unfair, but it was great fun trying to work this out over several sessions with a friend!
Our verification is based on symbolic execution, miri is an interpreter (concrete execution). So (at least in theory), our approach is more general. We have considered miri in relation to counterexamples: when Prusti emits an assertion failure and gives an example set of values that would lead to such a failure, we could use miri to make sure the counterexample is not spurious (which could happen with certain loop invariants IIRC). However, we have not implemented anything concrete yet.
Currently they are not handled. But (you guessed it) we also have a project working on this: attaching trusted specifications to external methods.
In the long term we might investigate a full integration with external verifiers, e.g. to check that the specifications declared on external methods in Rust is justified by their actual implementation, say in C. This is tricky because the specification language/level of abstraction might differ. It might be necessary to prove program refinement, for example.
We are working on improving the error reporting for the IDE extension. Regardless of the audience, Prusti is based on the Viper verification framework which is mainly implemented in Scala.
The two tools address similar problems. The kinds of properties you can prove (automatically) should also be similar, because both Prusti and Liquid Haskell ultimately use an SMT solver to check if assertions hold.
From what I have seen LH focuses on integrating into the type system (it is Liquid as in the 2008 Liquid Types paper). Generally it is possible to rewrite properties attached to a type to contracts, e.g. a non-zero Int input becomes a precondition that says that argument is non-zero. Checking termination with Prusti is also something we are working on.
This is an active research topic in our group. Within unsafe Rust code you lose the guarantees of the Rust ownership type system, which are important for framing (figuring out which parts of the memory _could_ be affected by the given operations). As a result, for e.g. pointer-manipulating unsafe code, the code will probably need to be annotated more heavily, to track which values are "owned" by whom etc.
The short answer is: it could be used for that. But there's a couple of things to say:
- Prusti is doing _modular_ verification: every method is verified in isolation, and all calls in that method's code only use the contracts declared on the call targets. This is good for scalability and caching and it means that a method's signature + contract is the entire API (you don't depend on its internals).
- Methods without a contract are assumed to have the precondition `true` and postcondition `true` (in other words, such a method can always be called and makes no guarantees at all about what it did to its mutable arguments or result). For methods declared within the current project, this is fine: if they could panic, Prusti would identify this when verifying them and the user would have to declare a precondition. For external methods (whose implementation is not verified), this is potentially unsound.
- However, we are in the process of creating a library of specifications for stdlib methods. We use a large-scale analysis framework (rust-corpus/qrates) to evaluate which methods are used most often. We try to specify such methods first to cover real-world Rust code usages.
Making the default precondition for external functions "false" (unless specified otherwise) would be sound but would be quite restrictive. One goal of Prusti is also incremental verification: you should be able to start using Prusti for basic checks then gradually introduce more specifications to get stronger and stronger guarantees about the program's behaviour.
Yes, we could improve the wording -- suggestions and users are welcome! The tool is indeed much more general purpose than integer overflows: it is a based on a deductive verifier which uses symbolic execution to figure out which nodes in the CFG are reachable and under what conditions. panic!, unreachable!, failed assert!s, etc are all checked. If one can be reached, the error to show to the user is reconstructed from the compiler's span information.
Some work to look at, if you are curious: Event-B, Trillium, IronFleet