Aurel300

5 ms·

1.
Show HN: A virtual machine in the Rust type system(github.com)
2 points by Aurel300 7mo ago|0 comments
2.
by Aurel300 2y ago
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
3.
by Aurel300 2y ago
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 crash
4.
by Aurel300 4y ago
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
5.
by Aurel300 4y ago
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 fail
6.
by Aurel300 4y ago
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 che
7.
by Aurel300 4y ago
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.
8.
by Aurel300 4y ago
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
9.
by Aurel300 4y ago
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 opera
10.
by Aurel300 4y ago
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 dec
11.
by Aurel300 4y ago
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 th
12.
by Aurel300 9y ago
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 f