Live data from Hacker News

My unusual hobby

stephanboyer.com

101–110 of 157 posts

Re: My unusual hobby

#101

Earlier quoted context omitted.

> Putting aside their steep learning curve, formal proof methods do not guarantee that the code you've written is bug free. People seem to always bring this up but what's better? Verified code is about as close as you're ever going to get to bug free. If you're doing a large proof, getting the specification wrong and not eventually noticing while working on the proof isn't common. You'll likely have something that is…

> Verified code is about as close as you're ever going to get to bug free. Code verified by legible proofs is safer than merely verified. The quality of the verification language matters, it's not only the programming language.

> Code verified by legible proofs is safer than merely verified. The quality of the verification language matters, it's not only the programming language.

If the specifications are human legible though, why do you care if the proof (which is checked for you by the machine) is legible? The main point of formal methods is to remove any doubt there are errors in the proof so it's an order of magnitude safer than relying on a readable hand written proof.

If you want a formal proof that is as readable as a hand written proof, you'd have to rely on a lot of automation going on in the background as every proof step must be traced back to basic axioms so complete proofs are pretty much always going to verbose and unreadable.

Re: My unusual hobby

#102
post #41

So I'm wondering what is the bridge between "proof-assistant" and "automated (or partially automated) theorem prover". As someone with "journalistic" (but fairly in-depth) knowledge about these topics, my guess is that something like a proof-assistant will have to be paired up with some kind of logic programming system (like Prolog, or a kanren-derived system or something). I guess then the problem of combinatorial e…

I also enjoy creating proofs as a hobby. When I'm doing it for fun, I tend to use Metamath, in particular, the "Metamath Proof Explorer" (MPE, aka set.mm) which formalizes the most common mathematical foundation (classical logic + ZFC). You can see that here: http://us.metamath.org/mpeuni/mmset.html

Here's a short video intro about MPE that I made: https://www.youtube.com/watch?v=8WH4Rd4UKGE

The thing I like about Metamath is that every step is directly visible. Coq, in contrast, shows "how to write a program to find a proof" - and not the proof itself. So you can see absolutely every step, and follow the details using simple hyperlinks.

Of course, all approaches have pros and cons. Metamath has some automation; the metamath and mmj2 programs can automatically determine some things, and there's been some experiments with machine learning that are promising. However, Coq has more automation, in part because it operates at a different level.

Re: My unusual hobby

#103

Earlier quoted context omitted.

Can you provide an example of a system being marketed as a tool to write "bug free code"? I saw nothing of the sort in the sites of Coq, TLA+ or Isabelle. Are you sure you're not the one arguing against a strawman?

In these comments there are several examples of folks selling an algorithm as "proven" and later turning out to be buggy.

Right, because they are proven. It's your assumption that proven == bug-free that is incorrect.

Re: My unusual hobby

#104
post #82

I've read a fair bit about functional programming but the right-associative nesting of -> still bothers me. (first precondition IMPLIES (second precondition IMPLIES (implication)) is inherently harder for me to understand than (first precondition AND second precondition) IMPLIES implication even though logically they are the same. The first version carries more mental overhead because it seems to indicate that there…

I am not a particularly experienced functional programmer. What functional programming I do is mainly relegated to code I write as a hobby, but in the last year or so I've started using more functional techniques at work (and luckily my teammates haven't lynched me yet). These days at work I use primarily Ruby and I've been surprised at how often I write curried procs. The language neither requires nor encourages that behaviour, so why am I doing it?

I think I started with the same assumption that you have: the order or parameters is arbitrary. In functional programming, though, this is not the case. For example, the "map" function takes a function and a functor (you can think of a functor as a collection like a list if you aren't familiar with the term). The order is important because if I partially apply a parameter to "map" I get a completely different meaning.

If you partially apply the function to "map", then the result is a function that applies that function to any kind of functor. If you partially apply the functor to "map", then the result is a function that applies any kind of function to that specific functor. Because I can only partially apply the first parameter in the function, this helps define the meaning of the function. In this example, the first definition is more correct (because "map" always takes the function first and the functor second). This becomes increasingly important as you build applicatives and monads.

In case that was unclear, here's a quick example. Let's say I have a list of integers and I have a function that adds 5 to an integer. If I do something like "map addFive list", it will go through each element in the list and add 5, resulting in a new list. If I partially apply the function to map with "map addFive", this will return a function that loops through any list and adds five to each element. So I might say "let addFiveToEach = map addFive".

If we had a different kind of map function (let's call it "mapNew") maybe we can do "mapNew list addFive" and it will do the same as the "map" code above. But if I partially apply list to mapNew I get a function that applies a function to my specific list. I might do "let eachInList = mapNew list".

The result is two very different functions. Either I will do "addFiveToEach list" or I will do "eachInList addFive". What meaning I prefer depends on the situation.

It's this idea that partially applied functions have a meaning that is powerful. When you are writing the code, which meaning do you want? As you note, both are possible, but I think you'll find that only one is actually appropriate in most cases. For example, instead of calling the function with both parameters, what if you assigned the result of partially applying the function to a variable? What would the variable be called? Does that help the reader understand the code?

Like I said, I was surprised at how often it makes a difference in my code. In fact, where it doesn't make a difference, it's usually an indication that I've made a mistake somewhere. It is even to the point where you start to want to pass partially applied functions around because they are more meaningful than the data that they contain. In fact a function is literally just another container in a functional programming language. For me, that was a kind of mind blowing realisation.

Re: My unusual hobby

#105
post #15

Earlier quoted context omitted.

Nothing guarantees that code is bug free. We will always have to interact with hardware, and although we can have high confidence in the hardware the physical world has a habit of changing out from under us. Your argument is very strange. We use type systems not because we think we'll write perfect code, but because we know it will reduce the likelihood of making mistakes in our code (at least, when that type system…

The problem is that these formal proof systems are often marketed as tools to write "bug free code". You will see statements along the lines of "this code is proven to be bug-free", etc. They over-sell and under-deliver. When you also consider that performing these proofs takes a very significant amount of time, you end up with something with very limited applicability for the vast majority of software development sc…

You mean like, say, seL4? Pretty sure that kernel is seeing some very real "applicability".

Re: My unusual hobby

#106
post #59

Earlier quoted context omitted.

> I haven't heard of any examples of complex verified programs where later someone found a huge flaw in the specification. Look at > https://www.krackattacks.com/ "The 4-way handshake was mathematically proven as secure. How is your attack possible? The brief answer is that the formal proof does not assure a key is installed only once. Instead, it merely assures the negotiated key remains secret, and that handshake m…

> I personally would consider this as a clear example of a huge flaw in a specification where a correctness proof was done on. Awesome, thanks for the recent example. My point is people seem to always bring up that specifications may have flaws as if this makes verifying code pointless. The guarantee of correctness is still an order of magnitude better than e.g. using unit tests and I'd wager it isn't common that spe…

> The WPA2 flaw is an example of a specification missing an important property as opposed to a property being described incorrectly.

If a specification misses an important property it is in my opinion by definition an incorrect description (in particular in this case when this missing property indeed leads to a security problem).

> I'd wager it isn't common that specifications are wrong in a critical way.

> People seem to jump on the latter the most I find as if it's common.

Let me present you an hypothesis: Currenly few things are really formally specified. And if it is done, there are usually very smart people behind the project. Which by definition makes it rare that they contain lots of critical errors. On the other hand, if these methods were applied "large scale" (i.e. also by much less skilled programmers who don't have a lot of deeper knowledge about more than basic computer science topics), the rates of errors in specification would be much higher and I believe this could become a not-that-uncommon topic.

Of course I nevertheless believe that if a lot more properties were formally specified and correctness proofs were done, the error rates of programs would nevertheless go down by magnitudes. But I don't believe that formal specifications and formal correctness proofs are a panacea. What I rather consider as sad is that it seems to be that if formal specification and machine-checked proofs were applied "by nearly every program", we actually slowly get out of ideas what kind of tools we can develop to decrease the error rates even more...

Re: My unusual hobby

#108
This is how I imagine Flowtype works for Javascript (more or less). What's interesting to me, is that this could be the foundation for AIs taking over programming from developers.

Re: My unusual hobby

#109

Cool post! The stuff about Curry-Howard was really interesting and relates to a question i have been thinking about. But I'm a novice when it comes to the theory of type systems or theorem provers. Maybe someone here can enlighten me? As type systems become more complex (like say in Scala or Haskell), they move towards having specialized syntax and weird hacks to express what are arguably simpler logical theorems/inv…

> so why can't we have a programming language that gives you a full blown logic system Most dependently typed programming languages, including Coq, give you the ability to basically "do logic" in a mostly unrestricted way. There are a few challenges that come to mind with making a practical programming language that can also do arbitrary math: a) For the language to be useful for proving things, it needs to be strong…

> I believe Coq uses a variant of a bidirectional type inference engine, which is quite usable in practice.

Edit (too late to edit the original comment): After thinking about the kinds of type errors I've seen in my proofs, I think Coq's inference algorithm is based on unification (not bidirectional?). Whatever it is, it's quite nice to work with in any case.

Re: My unusual hobby

#110
post #82

I've read a fair bit about functional programming but the right-associative nesting of -> still bothers me. (first precondition IMPLIES (second precondition IMPLIES (implication)) is inherently harder for me to understand than (first precondition AND second precondition) IMPLIES implication even though logically they are the same. The first version carries more mental overhead because it seems to indicate that there…

I am not a particularly experienced functional programmer. What functional programming I do is mainly relegated to code I write as a hobby, but in the last year or so I've started using more functional techniques at work (and luckily my teammates haven't lynched me yet). These days at work I use primarily Ruby and I've been surprised at how often I write curried procs. The language neither requires nor encourages tha…

> In functional programming, though, this is not the case.

That's an artifact of the language, not inherent to functional programming.

(I had a longer response in mind, might write it up later when I get time.)

Post reply on HN