Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Why don't people use formal methods? (2019)

hillelwayne.com

Post reply on HN
Print view View original

91–100 of 121 posts

Re: Why don't people use formal methods? (2019)

#91

Post by tombert »

lioeters wrote: post #90
tombert wrote: post #87

Earlier quoted context omitted.

I'm not familiar with any general purpose TLA+->regular code exporter. I think there are a few proof of concepts but as far as I'm aware nothing that has been seriously suggested for production. I do audit the code it generates, but ultimately all I'm concerned about is the algorithm a lot of the time and since the transformation it's been generally ok. I feel like coding errors and implementation-of-the-spec errors…

> would be an issue even if it were humans writing I see what you mean, that the conversion of TLA+ specs to code is error-prone in any case, regardless of who or what does the conversion. From what I've heard, an advantage of Lean over other major theorem provers is that it can generate actual executable code (apparently C), so you get the best of both worlds: formally proven specification and the implementation. In…

I've never used Lean, but as stated Isabelle has a code exporter as well; I was working with the Haskell exporter when I was doing grad school, and obviously Haskell is directly executable. It's a pretty neat thing, though it's still not perfect.

For example, a lot of mathematical types aren't actually directly translatable to programming languages. For some stuff, there is a "close enough" mapping to the type that works for most realistic cases, e.g. integers -> Int64. Other types become considerably more irritating; you might prove something with regards to all real numbers, but when exporting to a "real" programming language, there really isn't such thing as "real" numbers, since computers can really only do the rationals. You could export to float64, but then you're dealing with IEEE rounding, which may or may not be fine for what you're working on. You could use something like GMP (which is what I ended up doing when I had this issue) but of course you pay a performance penalty by doing that, and of course you're then trusting the correctness of GMP (though there is a verified subset, to be fair).

I feel like with TLA+, I am typically working on higher-level problems. Usually I'm modeling distributed systems, which sort of inherently requires an "opinion" for deployment.

How would I deploy this code? Erlang? Kubernetes? Docker Swarm?

How am I doing service discovery? DNS? YOLOing with raw IP addresses?

Suppose my model has a global function [1] that I'm writing to as a global shared store? Where does this live? Is this a local cache? Is this Redis? Memcached?

I could go on. The whole point of TLA+ is to write and test the algorithms, and very purposefully allows and encourages you to ignore details that aren't necessary to show correctness of your algorithm.

I'm not saying you couldn't do this, to be clear. You could absolutely create an exporter for TLA+, but my point is that it would require a good chunk of opinions and decisions to do it. You'd also need to ensure that the semantics of these things properly map to your model, else the exporter is only of debatable utility.

I think this is why there isn't really a serious exporter for TLA+. You just work at a different level with it, and I think there are just too many (kind of arbitrary) decisions that would have to be made in order to do anything useful.

[1] In TLA+, "function" basically means key-value map.

Re: Why don't people use formal methods? (2019)

#92

Post by exogenousdata »

s_dev wrote: post #2

https://blog.janestreet.com/formal-methods-at-jane-street-in... I thought this article from Jane Street makes a nice complimentary pairing.

And it’s not just blogs. They’ve got an open job posting [0] for a ‘Formal Methods Engineer’.

[0] - https://www.janestreet.com/join-jane-street/position/8585303...

Re: Why don't people use formal methods? (2019)

#93

Post by lioeters »

tombert wrote: post #91
lioeters wrote: post #90

Earlier quoted context omitted.

> would be an issue even if it were humans writing I see what you mean, that the conversion of TLA+ specs to code is error-prone in any case, regardless of who or what does the conversion. From what I've heard, an advantage of Lean over other major theorem provers is that it can generate actual executable code (apparently C), so you get the best of both worlds: formally proven specification and the implementation. In…

I've never used Lean, but as stated Isabelle has a code exporter as well; I was working with the Haskell exporter when I was doing grad school, and obviously Haskell is directly executable. It's a pretty neat thing, though it's still not perfect. For example, a lot of mathematical types aren't actually directly translatable to programming languages. For some stuff, there is a "close enough" mapping to the type that w…

That's illuminating, thank you for a generous reply. The point about real numbers and their representation (or lack thereof) in programming languages is a great example of the gulf between mathematics and programming. I understand that for most languages, there can be no direct correspondence between a mathematical proof and the program that implements it.

In a recent discussion about the paper "How real are real numbers?" by G. J. Chaitin, someone mentioned that there seems to be a trend of a "computational" approach to mathematics on one hand, and from the other side, a "mathematization" of computer programming. With the rise of language models and their ability to generate correct programs, I imagine there is a pressing need to bridge the gulf between the two fields. Not only to verify the correctness of programs written in existing languages, but to design languages where that need for verification is taken into considertaion from the ground up, maybe close to Rust where the compiler refuses to compile a program that cannot be verified to be correct.

A common complaint about software engineering is that it is not "engineering" as a formal discipline; and about computer science that it is not a "science" (nor is it about computers, any more than astronomy is "telescope science" and biology is "microscope science" [^1]). It seems to me that a firmer grounding in mathematics, particularly in programming language design, would be helpful in improving the situation, so that software is actually "engineered" based on immutable truths and logic, and verified to be correct.

And how would the computational approach to mathematics influence it as a discipline.. Perhaps it may bring the field closer to a "science" with more experimental exploration.

[^1]: I think attributed to Vinton Cerf in _Where Is the Science in Computer Science?_. https://cacm.acm.org/opinion/where-is-the-science-in-compute...

Re: Why don't people use formal methods? (2019)

#94

Post by pocksuppet »

teiferer wrote: post #19

To me, "this returns sorted lists" illustrates the crux. You may know exactly what you want, and you may have a reasonably fast and cheap way to verify your code against a formal specification. But the formal specification needs to come from somewhere and for any non-trivial program its complexity is going to be in the same order of magnitude as the code implementing it. So we are back to writing "code" (which is wha…

Actually, sorting a list is an example of something really easy to specify: for each pair of two elements, the one that comes first is less than or equal to the one that comes second.

Re: Why don't people use formal methods? (2019)

#95

Post by IshKebab »

win311fwg wrote: post #70
IshKebab wrote: post #64

Earlier quoted context omitted.

It's a continuum... but I would say even Rust's type system is not in the realms of "formal verification". I think you need at least some kind of refinement types so you can say "an integer between 1 and 10" before you can stake even a vague claim to "formal verification". So I don't think you can say it's common in the software world.

Specifying that a value must be an integer between 1 and 10 is most certainly further along the continuum than only specifying that a value must be an integer, but both define a theorem about the program that can be validated. How is the latter not formal verification? It's the same thing, only differing by degree.

As I said, it's a continuum. I'm drawing the line somewhere further along it than Rust's type system.

Re: Why don't people use formal methods? (2019)

#96

Post by Jtsummers »

pocksuppet wrote: post #94
teiferer wrote: post #19

To me, "this returns sorted lists" illustrates the crux. You may know exactly what you want, and you may have a reasonably fast and cheap way to verify your code against a formal specification. But the formal specification needs to come from somewhere and for any non-trivial program its complexity is going to be in the same order of magnitude as the code implementing it. So we are back to writing "code" (which is wha…

Actually, sorting a list is an example of something really easy to specify: for each pair of two elements, the one that comes first is less than or equal to the one that comes second.

> for each pair of two elements, the one that comes first is less than or equal to the one that comes second.

That's the property that the result is sorted, but not that you've performed the desired task of sorting a particular list. You also need a post-condition saying that each item in the original is in the destination and with the same number of occurrences.

If you just require that the result be sorted, then this is a valid sort:

  def sorted(ls):
    return []
If you require that it be sorted and contain the same items (but don't check the count), then this is technically sufficient (I've abstracted the actual sort operation out):

  def sorted(ls):
    ls = list(set(ls)) # removes duplicates
    # perform sort
    return result
If you get to the right post-condition, it has to have the same items and the same count and be sorted, then it will satisfy this test:

  def sorted_postcondition(original, result):
    return all(x

Re: Why don't people use formal methods? (2019)

#97

Post by win311fwg »

IshKebab wrote: post #95
win311fwg wrote: post #70

Earlier quoted context omitted.

Specifying that a value must be an integer between 1 and 10 is most certainly further along the continuum than only specifying that a value must be an integer, but both define a theorem about the program that can be validated. How is the latter not formal verification? It's the same thing, only differing by degree.

As I said, it's a continuum. I'm drawing the line somewhere further along it than Rust's type system.

Understood. In dynamic verification, does that same line hold? Or would you say it is it unique to formal verification? If so, why?

Re: Why don't people use formal methods? (2019)

#98

Post by antonvs »

mrkeen wrote: post #74
taybin wrote: post #41

I would love to see an example of a proof for something like a text editor. How can people be expected to do this when the examples are always trivial toys, like array sorting? Show me a formal proof of something that in the trenches programmers can copy from. A proof of a basic todo list or something like that.

> A proof of a basic todo list or something like that. Just using a verb here would be a first step toward rigorous thinking. A proof that a todo list does what?

I have a proof that shows that most of what you put on your todo list, you won't do. Please let me know where I should collect my Nobel Prize.

Re: Why don't people use formal methods? (2019)

#99

Post by antonvs »

taybin wrote: post #89
mrkeen wrote: post #74

Earlier quoted context omitted.

> A proof of a basic todo list or something like that. Just using a verb here would be a first step toward rigorous thinking. A proof that a todo list does what?

To-does. Just like how a butler buttles.

Excuuuuuse me, I believe that should be to-dos.

Re: Why don't people use formal methods? (2019)

#100

Post by antonvs »

warkdarrior wrote: post #60
taybin wrote: post #41

I would love to see an example of a proof for something like a text editor. How can people be expected to do this when the examples are always trivial toys, like array sorting? Show me a formal proof of something that in the trenches programmers can copy from. A proof of a basic todo list or something like that.

My guess is that the formal spec for a basic TODO list app is the same size as the source code of the app itself.

I would not be even slightly surprised if it were larger.
Post reply on HN