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

My unusual hobby

stephanboyer.com

Post reply on HN
Print view View original

71–80 of 157 posts

Re: My unusual hobby

#71

Post by guizzmo »

jloughry wrote: post #64
sillysaurus3 wrote: post #57

How do you pronounce Coq? I searched it but all I found was https://m.youtube.com/watch?v=TAHH83n2dmY

It's pronounced like "cock". It's named after the animal, and that's how you say it in French. It's how people who use the tool say it.

So there is this rumor hanging around the french community that use Coq, that the name was deliberately chosen to sound like "cock" in english. This way, french researcher could brag to other collegues about going to a conference about "cock", in all seriousness.

Re: My unusual hobby

#72

Post by raphlinus »

fizixer wrote: post #53
raphlinus wrote: post #46

Earlier quoted context omitted.

I've done a bit of work on a "next generation" Metamath, Ghilbert[1], but have come to the conclusion that it's too ambitious to do as a part-time project. People might find it interesting, though, because it attempts to take interactivity to a higher level than Metamath, and is (imho) a cleaner language. [1] http://ghilbert.org/

Hey glad to find someone involved in metamath related project. I guess if I could simplify my discussion to one question, it would be: Does metamath or ghilbert use a logic inference engine to automate parts of a proof? The way I understand metamath (the website, not the language) is that it's like an encyclopedia of mathematical knowledge. The encyclopedia is in the form of theorems, lemmas, corollaries, and their p…

Metamath basically goes in the other direction than most proof assistants, it relies on human ingenuity. There is a bit of search in the original C metamath (the "improve" feature) and also just a tiny amount in mmj2 (unification), but if the user doesn't have a clear picture what the fine-grained steps are, they're going to have a bad time.

One of the interesting things about Metamath is that proofs tend to be very concise. In more automated proof systems, you use automated tactics and proof search techniques, and if you expanded out their output, they'd generally be quite verbose. I think this has led a lot of people to believe that automation is more necessary than it actually is.

All that said, you absolutely could build an inference engine of similar scope as the other big proof assistants, and use the existing Metamath database as a rich foundation.

Happy to answer other questions.

Re: My unusual hobby

#73

Post by icebraining »

david-gpu wrote: post #26
voxl wrote: 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…

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?

Re: My unusual hobby

#74

Post by sls »

jloughry wrote: post #64
sillysaurus3 wrote: post #57

How do you pronounce Coq? I searched it but all I found was https://m.youtube.com/watch?v=TAHH83n2dmY

It's pronounced like "cock". It's named after the animal, and that's how you say it in French. It's how people who use the tool say it.

Not really, the English word "cock" has a very different vowel than the French "coq" - https://youtu.be/bIraCzL3dtI?t=4s is a pretty fair exemplar. It's a lot more like the "o" in "joke".

(edit: maybe you're English? Some English accents of England would articulate "cock" very close to French "coq" and "joke" would be far away. Apologies, one really does need to specify which "English" is meant, and I should have seen that at once. First cup of coffee still in progress.)

Re: My unusual hobby

#75

Post by jacquesm »

eqmvii wrote: post #56
j2kun wrote: post #5

> What's really amazing to me is that Stephen Kleene probably proved this without the help of a computer, but I was able to verify it with the highest possible scrutiny. It's as if he wrote an impressive program without ever having run it, and it turned out not to have any bugs! This offhand comment (which we can all forgive) makes it seem like mathematics happens in a vacuum. I can understand the temptation to think…

> Mathematicians don't just write down a proof and cross their fingers. On the flip side, this is exactly what a lot of lawyers do when writing contracts. Not necessarily maliciously or negligently, but it can still make for fun questions of interpretation when things don't go as expected.

There is a nice parallel between the legal profession and programming. Programmers write software in such a way that they try (if they're any good) to reduce the number of assumptions made and the number of bugs and the ambiguities in their code. Failure to do so results in undefined behavior, crashing code and in internet facing code in possibly being hacked.

Lawyers write code into contracts. Good lawyers try to do so by removing ambiguity where ever they can. Failure to do so results in court cases where that ambiguity is resolved, and in some cases will result in damage for the party that originally contracted them to write the code.

Neither lawyers nor programmers are legally liable for such fuck-ups.

Re: My unusual hobby

#76

Post by iamrecursion »

curryhoward wrote: post #32
zaptheimpaler wrote: post #22

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 should add that something like FStar [0] combines the capabilities of automated theorem proving and a more manual-proof-based dependent type system like that in Idris.

It doesn’t have some of the power of Idris’ elaborator reflection, for example, but it can eliminate many long-winded manual proofs via the SMT solver.

[0] https://www.fstar-lang.org/

Re: My unusual hobby

#77

Post by Turing_Machine »

seanwilson wrote: post #30
david-gpu wrote: post #2

I had to take a semester on formal proofs using Coq, the same tool the article talks about. Putting aside their steep learning curve, formal proof methods do not guarantee that the code you've written is bug free. They only guarantee that the code follows the requirements you defined given the conditions you also set on your inputs. You can think of it as a mathematical proof of your postconditions will hold given th…

> 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…

"People seem to always bring this up but what's better?"

"Better" is a slippery term. Code doesn't exist in a vacuum, but rather in an external world that has other constraints (e.g., time and budget).

If using formal proofs means that you go through one development cycle while your competitor is iterating three, four, or five times, your milkshake is going to be drunk.

Re: My unusual hobby

#78

Post by almonj »

Text Advertising - See The Twilio® Advantage - twilio.com‎ Adgo.twilio.com/Text/Advertising‎ Designed for Developers, Simple Pay as You Go Pricing—Talk to a Specialist Now! Get A Free API Key · Automatic Volume Discount · Global Infrastructure · Talk To An Expert Today Types: Call Tracking, Lead Alerts, Text Message Marketing, Phone Number Lookup

    MessagingProducts & PricingShort Codes for SMS & MMSSMS PricingContact Twilio

Re: My unusual hobby

#79

Post by pron »

zaptheimpaler wrote: post #22

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…

We do have such languages. For example, Java has JML [1], C has the very similar ACSL, and a programming language like Idris has a type system that can express arbitrary logical propositions (there are various tradeoffs that may influence the choice between a rich type system a-la Idris or a rich contract system a-la JML, but many of the principles are the same).

The problem is that we do not yet know how to make effective use of such code-level specifications. Finding a cost/benefit sweet spot is not easy (I personally prefer the JML approach precisely because I think it allows for greater flexibility in the choice of tradeoffs vis-a-vis confidence vs. cost).

[1]: http://www.openjml.org/

Re: My unusual hobby

#80

Post by wildmusings »

jacquesm wrote: post #75
eqmvii wrote: post #56

Earlier quoted context omitted.

> Mathematicians don't just write down a proof and cross their fingers. On the flip side, this is exactly what a lot of lawyers do when writing contracts. Not necessarily maliciously or negligently, but it can still make for fun questions of interpretation when things don't go as expected.

There is a nice parallel between the legal profession and programming. Programmers write software in such a way that they try (if they're any good) to reduce the number of assumptions made and the number of bugs and the ambiguities in their code. Failure to do so results in undefined behavior, crashing code and in internet facing code in possibly being hacked. Lawyers write code into contracts. Good lawyers try to do…

>Neither lawyers nor programmers are legally liable for such fuck-ups.

Lawyers can be held liable if they do a horrible enough job. Likewise for programmers, and there are a lot of people advocating for strict liability for software defects in commercial products/services.

Post reply on HN