undefined | Better HN

0 pointsvlovich1233y ago0 comments

Personally it’s because I don’t enjoy solving the problem once in one language and then transcribing it into a totally different language and worrying I got the transformation correct (+ I still need to write all the same tests). Also, afaik proof languages don’t have libraries for building up more and more proofs, and, even if they did, they’re not going to come bundled with random runtime dependency X I picked to implement it. It doesn’t feel like it will be an enjoyable experience and there’s generally little incentive from the buyer’s end (ie management aren’t typically demanding it / hiring for it / giving time in the schedule to write proofs).

And as far as it helping with other languages, I feel like practical TypeScript understanding doesn’t benefit particularly from proofs. Rust and Haskell I can’t make claims about but if that’s true those languages will suffer (but I don’t think it’s really needed).

0 comments

5 comments · 2 top-level

BreakfastB0b3y ago· 2 in thread

I didn't mean to imply that people should be using Coq or another proof assistant in their development workflow. More that understanding formal verification aids in thinking about typed programs.

However no type system of a Turing complete programming language can ever be truly trusted as a proof system because looping forever or other non-termination can be used to prove any proposition.

  const proveAnything = <A>(): A => proveAnything()

The above function can prove any proposition including 1 == 2, by just recursing forever.

However, take Rust's ownership system for example, it uses a type system that corresponds to a kind of logic called a sub-structural logic that denies one of the axioms of typical classical logic systems, namely, the weakening axiom, e.g. a function of the type

  fn <A>(a: A) -> (A, A) { ... }

is not possible to write in Rust, but easily writable in most other programming languages. Because of this, Rust is able to "prove" that the program is free from data races which is pretty cool if you ask me.

tatref3y ago

Can't the function just return `(a.clone, a.clone())`?

Maybe you mean something like this? `fn extend_vec(to: &mut Vec<i32>, from: &Vec<i32>) { ... }`

This does not compile if you pass the same Vec as to and from, because of the `&mut`

brabel3y ago

Without a trait bound that demands cloneable items, no.

themulticaster3y ago· 1 in thread

Before I begin - I hope my comment doesn't come across as too confrontational. I don't want to invalidate your experience, but I'd like to spread information about formal verification techniques that are usable today.

> Personally it’s because I don’t enjoy solving the problem once in one language and then transcribing it into a totally different language and worrying I got the transformation correct (+ I still need to write all the same tests).

Isabelle/HOL [1] allows specifying and proving properties about a function/program in Isabelle/HOL and then generating output in Haskell, OCaml, Scala and SML. Granted, you'd need to learn Isabelle/HOL, but you wouldn't need to worry about the transformation process.

> Also, afaik proof languages don’t have libraries for building up more and more proofs, and, even if they did, they’re not going to come bundled with random runtime dependency X I picked to implement it.

The Archive of Formal Proofs [2] is a collection of Isabelle theories (proof modules) that you can easily integrate into your own proofs. Some proofs in the AFP are about specific properties so they're not that interesting as a proof library, but many others include reusable specifications that are useful in other proofs.

I'm not quite sure about the runtime dependency aspect you mention. In general, proofs about data structures and algorithms are interesting, but proofs about glue code or I/O interfaces are mostly useless and a waste of time (depending on the context). For example, proving your sorting algorithm is correct is a good fit for formal verification, but proving your network code uses the correct flags in a socket creation syscall is hardly interesting and provable.

I'm only familiar with Isabelle/HOL, so my comment is limited to that environment.

[1] https://isabelle.in.tum.de/overview.html

[2] https://www.isa-afp.org/

vlovich123OP3y ago

I didn't mean to disparage your post nor did I intend to come across as angry if that's how it landed (sorry). You just asked the question of "why isn't this done more often" & I was adding my perspective.

> Isabelle/HOL [1] allows specifying and proving properties about a function/program in Isabelle/HOL and then generating output in Haskell, OCaml, Scala and SML. Granted, you'd need to learn Isabelle/HOL, but you wouldn't need to worry about the transformation process.

These languages are not the most commonly ones used in the industry (Java, C#, JavaScript/TypeScript, C/C++, Rust, Python etc). I'm particularly interested in C++ and JavaScript/TypeScript if you know of any.

> I'm not quite sure about the runtime dependency aspect you mention. In general, proofs about data structures and algorithms are interesting, but proofs about glue code or I/O interfaces are mostly useless and a waste of time (depending on the context). For example, proving your sorting algorithm is correct is a good fit for formal verification, but proving your network code uses the correct flags in a socket creation syscall is hardly interesting and provable.

What I was saying is that you may have a distributed system that makes up multiple components. Usually each component individually is already pretty hardened. The errors indeed pop up in the glue code where you're sending messages between those distributed components. Less so about the correct flags in socket creation but "did you remember to handle error case X?", "did you manage the state transitions correctly for distributed messages?", "is the custom caching layer I layered on top of the distributed component interacting correctly with that component?", "did I correctly implement 2PC?", etc. For example, imagine that you used YuggabyteDB. YuggabyteDB may have proofs around its behavior. However, if I want to write a proof for my usage of it, I'm going to have to pick generic components that describe a "distributed database" and customize what kind of isolation level I'm expecting between transactions. Some of this can be expressed generically and maybe there are such components already written. Some of the stuff those is extremely nuanced like "DB X implements operation Y in a nuanced way".

I'm not saying these are all necessary for the purposes of getting value out of type checking. I am suggesting that the difficulty for type checkers to be used in that way, the lack of proof "APIs" for components, the challenge of dictating runtime language auto generation / manually translating is a reason you haven't seen a massive rush towards formal proofs I think.

j / k navigate · click thread line to collapse