Hacker News Reader

https://dafny.org/ also allows proof checking and allows do write real programs with it. It has a java like syntax and is also from MS I believe

Having used both Dafny and F* quite extensively, Dafny, and its predecessor Spec#, are simple and practical, thanks to being based on Hoare logic (contracts).

It's a great place to start with verification, as proofs are discharged to SAT/SMT, so things are automated. It can get a bit frustrating when automation is not able to prove things, that's the major disadvantage of SAT/SMT.

But it's not a toy. Some of the largest verification efforts have been done in Dafny. See e.g. IronFleet [1].

[1] https://www.andrew.cmu.edu/user/bparno/papers/ironfleet.pdf

F* also uses SAT/SMT, specifically Z3.

Sure, what I meant is that Dafny outsources everything to SAT/SMT. If it doesn't manage to prove things for you, it gets a bit frustrating as there is not much support for manual tactics compared to F*, Coq or Isabelle, which can also leverage SAT/SMT, but have other options.

Agree it’s not a toy. AWS implemented a large chunk of IAM in Dafny. Though IIRC they have their own non-public compiler to Java

I’ll add that SPARK Ada allows this now, has commercial tooling from Adacore, and was field-prove in years of commercial deployments.

https://en.m.wikipedia.org/wiki/SPARK_(programming_language)

It builds on the Why3 platform which also supports Frama-C for the C language. IIRC, SPARK can be compiled to C for C-only, runtime targets as well.

Do you think you might be able to elaborate a little bit more about this?

I was skimming the "Proof-Oriented Programming" book, and it seems that the primary way to execute F* programs is by extraction or trusted compilation (same as Rocq and Lean, for example). Does F* have some special way to work directly with realistic source code that these other systems don't?

F* is a programming language with proof support. Lean/Coq are theorem providers that can be used to model and generate code. In Coq, there's not a standard way to generate code, you might model and create code many different ways. F* seems to bring this in as the central goal of the language. So I'm discussing this structural difference. F* has an SMT solver, but Lean can import an SMT solver. So the goal is the important difference here - making theorem proving as accessible as possible in a real language. It's a move in the right direction, but we want to get to the point standard program languages have this support if you need it.

> F* is a programming language with proof support. Lean/Coq are theorem providers that can be used to model and generate code.

Lean is also a programming language with proof support. It is very much in the same category as F* in this regard, and not in the same category as Coq (Rocq).

In Rocq/Coq, you have "extraction", which is the standard way to compile programs. This is how the C compiler CompCert is executed, for example. So, all of these languages are in the same category in this respect.

> I studied formal languages for ~2 years and have professional experience programming coq. The real benefit of this language, over other formal languages is the focus on being able to write real programs in it.

How does Idris compare these days?

Where would a smooth brained CRUD app web developer who failed high school maths perhaps learn more about the point of this?

The point would be to prove that your database stays consistent, a DB upgrade wouldn't break, or that you could achieve 100% up time given certain assumptions. An automated solver/prover might even be able to tell you where in your program breaks this. Without a technology like this, you have to carefully read your program, but this is the methodology to make the computer deal with that. Unfortunately formal verification is mostly used for research, F* is framing itself as taking a step to bring that to production codebases. Unfortunately I don't know good resources, but as researchers adapt this technology, and as we automate a lot of the heavy mathematics, you'd never want a programming language without this option.

>memory safe (without a borrow checker)

This sounds like a very weird statement.

In my opinion, a proper proof-oriented language would inevitably contain a borrow checker variant as a subset of its functionality (assuming the language has notion of pointers/references and focuses on achieving "zero cost abstractions"). Lifetime annotations and shared/exclusive references provide essential information and code use restrictions which enable automatic proof generation.

After all, type and borrow checkers are nothing more than limited forms of automatic proof generation which are practical enough for wide use.