Interestingly, this also works:

let dynamicChecking () =
  assert false;
  write "demo/password" "junk"

… but not this:

let dynamicChecking () =
  assert false

I should have clarified that of course this works as expected:

let dynamicChecking () : ML unit =
  write "demo/password" "junk"

And so does this, for a different reason:

let dynamicChecking () : _ =
  write "demo/password" "junk"

#581

This kind of Pollack inconsistencies (e.g. #143, #581, #853) have been plaguing F* since its very beginnings, but things have been slowly getting better (e.g. purity is now the default most of the time). No proof of false here, just a very bad, recurring usability issue.

How to Believe a Machine-Checked Proof. Robert Pollack
http://ojs.statsbiblioteket.dk/index.php/brics/article/viewFile/18945/16584

Pollack-inconsistency. Freek Wiedijk
http://www.cs.ru.nl/F.Wiedijk/pubs/rap.pdf

For interactive theorem provers a very desirable property is consistency: it should not be possible
to prove false theorems. However, this is not enough: it also should not be possible to think that
a theorem that actually is false has been proved. More precisely: the user should be able to know
what it is that the interactive theorem prover is proving.

Is that better than defaulting to Tot? That is, won't the same inference happen on inner lets?

@nikswamy We've been staring in Paris at one more disturbing example of this kind:

(* this is accepted *)
let write (#a:Type) (r:ref a) = r := 42

(* this fails *)
(* let append_to (#a:Type) (xs:list a) = 2 :: xs *)

(* this works again *)
let append_to (#a:Type) (xs:list a) = ignore(alloc 5); 2 :: xs

We all found this very confusing. It took a while for us to realize that the difference between cases 1,3 and case 2 is caused by the fact that for pure things the default is Tot (so requiring a valid precondition), while for effectful things it's an effect with an arbitrary computed wp.

We think that the best solution for this would be to require valid preconditions everywhere by default, but have some way to explicitly ask F* to compute a wp. Clement is suggesting a syntax like this:

let write (#a:Type) (r:ref a) : STATE unit _ = r := 42

(which currently of course doesn't work since it's not type inference that should be filling the hole ... but this is just concrete syntax, anything like this would do)

Anyway, being able to explicitly ask F* to infer wps would still be very useful, so we're not big fans of requiring all top level definitions to be fully annotated.

PS: Another confusing thing here is that we were expecting (lax) type-checking to be more restrictive than ML type-checking for the same code, but in this case it's definitely not, in a way that interacts badly with parametricity too: the preconditions inferred for cases 1,3 are (at least intuitively) equivalent to a = int.

This issue is still there. So here's a crisper summary of the proposal here:

1. top-level stateful functions without an annotation are still allowed, but get True as the precondition, as it already happens for pure code ... which would already remove the confusion above.
2. we provide lightweight syntax for asking F* to infer a precondition (i.e. the current behavior), for instance:

let write (#a:Type) (r:ref a) : STATE unit _ = r := 42

3. One can of course still fully annotate pre-/postconditions, but one is still never forced to do so

For the record, as I'm sure you intended, this isn't specific to STATE. This would apply to any effect.

Recall that we used to have a notion of a default for each effect. e.g., St a = STATE a (fun p _ -> forall x h. p x h) used to be the default for STATE. That's analogous to your case 1 above. However, we removed support for default effects since we argued then that it was counterintuitive. I don't mind finding a way to restore them. I read part 1 of your proposal to mean that unannotated top-level code with inferred effect M a wp is checked against the default effect for M to M a (M.null_wp a).

For (2), that should work, with the caveat that inference is unlikely to work except when using an irreducible effect label. For instance, if you wrote let f (x:a) : ST b _ _ = e, it's very likely that the pre and post would be would not be inferred. You'd have to write it in WP form let f (x:a) : STATE b _ = e.

In the current state of the code, it is quite hard to support the STATE _ _ idea. The reason is related to the wp inference in the 2-phase typechecker.

@nikswamy suggested another way to solve the issue. For top-level, unannotated, effectful functions, we infer their wps, as we do right now, but additionally check that they have a trivial precondition. This gives us best of both the worlds -- surprises like assert False in the body of the function will be caught, and the postconditions of the function would still be available for the callers.

For example, this works:

module Test

open FStar.Ref

let incr (r:ref int) = r := !r + 1

let test (r:ref int) =
  let h0 = ST.get () in
  incr r;
  let h1 = ST.get () in
  assert (sel h1 r == sel h0 r + 1)  //possible because of inferred wp of incr

While this fails:

module Test

open FStar.Ref

let incr (r:ref int) = assert False; r := !r + 1  //no longer has a trivial precondition

with assertion failed.

In addition, collecting examples from the comments above, all of the following fail (look for expect_failure)

module Test

open FStar.Ref
open FStar.All

let f (_:unit{false}) : ML unit = ()

[@expect_failure]
let g () = f (); assert false

type filename = string

let canWrite (f:filename) = false

let write (f:filename{canWrite f}) (s: string) : ML unit =
  FStar.IO.print_string "A"

[@expect_failure]
let dynamicChecking () =
  write "demo/password" "junk"

[@expect_failure]
let dynamicChecking2 () =
  assert false;
  write "demo/password" "junk"

[@expect_failure]
let write2 (#a:Type) (r:ref a) = r := 42

[@expect_failure]
let append_to (#a:Type) (xs:list a) = 2 :: xs

[@expect_failure]
let append_to2 (#a:Type) (xs:list a) = ignore(alloc 5); 2 :: xs

What do you think? cc @cpitclaudel @catalin-hritcu, @s-zanella, @kkohbrok

I'd prefer to always require full annotation for top-level effectful definitions, but @aseemr's proposal is a good compromise.

I like this still much better than requiring annotations everywhere. Just to make sure I understand, compared to our original proposal, it's giving us 1 (and 3) but without the 2, right?

And if some people really like self-imposed discipline, maybe we can add a flag to make top level annotations required? --discipline? :)

@catalin-hritcu, yeah (1) and (3), but no (2).

The proposal from my last comment is implemented in F* master, here are the testcases: https://github.com/FStarLang/FStar/blob/master/examples/bug-reports/Bug1055.fst. Closing the issue, please reopen if needed.