FStar
FStar copied to clipboard
FStarLang
A Proof-oriented Programming Language
I've run into multiple Sys_error no such file bugs. Ideally for a user, it would not ask for a bug report when a file is missing. And it print just...
I would like to start discussion of FStar compiler distribution size. Currently package is 630 Mb or so. I build tooling to the F* for .NET land and publish compiler...
F* routinely gets new features and there's no good programmatic way of testing for them. We could support something like: ``` $ fstar.exe --list-features fstar.include context-pruning ... ``` and ```...
We usually do a full dependence scan when starting to verify a file, checking for cycles, and even looking past interfaces to find potential cycles. This is needed, of course,...
```fstar let foo () : GTot int = 123 let bar : int = foo () + 1 ``` This code warns like so: ``` * Warning 272 at G.fst(7,0-7,28):...
Consider the following (repetitive) module: ```fstar module Test #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open FStar.Mul assume new val u32: Type0 assume new val u16: Type0 assume new val...
For example: ```fstar val test: nat -> nat // note: no `rec` let test n = if n = 0 then 0 else test (n-1) ``` gives the error ```...
I just goofed up some lemmas by leaving an unused (i:nat) in the arguments. I missed this in validation as it does not warn (like to does nicely for rec...