Aurel300

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!

http://www.mcgov.co.uk/zahada.html

There were also some similar games/clones that never quite hit the spot for me.

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.

I have been using Haxe (not professionally, but still quite intensively) for more than 3 years now. I've moved to it from AS3.0 / Flash initially to make games. As I learnt the language more and more, however, I started using it for a very wide variety of projects - data scraping / mining / processing, websites, image processing, scripts, etc. It has a small but quite active community and it is really easy to get in touch with one of the core devs, suggest features, or even contribute to the project.

If I had to point out its biggest flaw, it would be a lack of in-depth documentation - the API reference is understandable, the manual explains the language features quite well, but if you want to do some more specific things with a less-used platform, for example, you might have to experiment a little bit. I think this is a consequence of having a smaller community for a project which targets such a large number of targets simultaneously. However, since you asked about games, Haxe is great for gamedev. There are multiple frameworks which allow you to develop cross-platform games very smoothly. There are many games popular on Steam that were written in Haxe: Papers, Please (NME); Evoland (OpenFL? not sure); Rymdkapsel (OpenFL); the upcoming Northgard (http://northgard.net/, using the new Hashlink target).

I am also playing around with writing a framework, though it's nowhere near completion. I've written many gamejam games in Haxe (http://www.thenet.sk/), with source code, if that interests you.

If you want to try something new – I recommend Haxe wholeheartedly, even if you decide not to use it, I think writing code in it is just fun.