I had the same argument with the Stanford Pascal Verifier people around 1980. They were using the SAIL PDP-10, with keyboards with extra characters and extra shift keys TOP and META. Assertions were written with mathematical notation but code was written in ASCII. We stuck to ASCII and Pascal operators for Pascal-F.

Today, everybody has Unicode output, and all the math symbols are potentially typeable, but it drives programmers nuts if they have to enter them. If you're going to do a verification system, you have to design it for programmers, not mathematicians, or it won't be used. This is a serious problem with formal methods. The formalism is a means to an end, not an end in itself. The end goal is bug-free code.

Dafny for Rust has potential. One big problem is where to put the assertions inside terse functional notation. This is word wrap in Rust:

    s.lines()
        .map(|bline| UnicodeSegmentation::graphemes(bline, true)   
            .collect::<Vec<&str>>())
        .map(|line| wordwrapline(&line, maxline, maxword))
        .collect::<Vec<String>>()        
    .join("\n")

OK, where would we put assertions? Maybe intersperse

    .assert(|arg| assertionexpression)

which is just a passthrough that returns its value but allows making assertions about what's going through it.

The screenshot shows what looks like the emacs mode which actually just masks the ASCII you type with the unicode characters to make it look nice. In practice you're just writing plain ASCII https://github.com/houli/verification/blob/master/strings3.d...