[HN Gopher] A gentle introduction to automated reasoning
___________________________________________________________________
A gentle introduction to automated reasoning
Author : mooreds
Score : 41 points
Date : 2022-02-19 19:10 UTC (3 hours ago)
(HTM) web link (www.amazon.science)
(TXT) w3m dump (www.amazon.science)
| systemvoltage wrote:
| Why do designers go out of their way to make text difficult to
| read? Amazon.science violates two things simultaneously: 1) Not
| using book-weight font 2) Not using pure black (or close to
| black) text on white background.
| mindcrime wrote:
| Note for anybody who's particularly interested in automated
| reasoning, and likes watching video - the UCLA Automated
| Reasoning Group has a ton of good stuff up on Youtube.
|
| https://www.youtube.com/c/UCLAAutomatedReasoningGroup
| sva_ wrote:
| This is from Dec 1st of last year (so not too long ago).
|
| It's nice to see private companies dive into the (automated)
| theorem proving and formal verification world, and I'm curious if
| throwing money at this will have a meaningful impact on the field
| (if that is what they're planning to do). It seems like we've
| slowly been getting to a point, where the tools we have available
| now might be combined in a way that makes some impressive
| progress on all this.
| nextos wrote:
| I have been thinking lately that perhaps in the future a lot of
| software will be built using DSLs, to enable cost-effective
| formal verification.
|
| Turing-complete languages have an excessively broad semantics,
| which makes it hard to prove things about programs written with
| them. An alternative would be to build tools that allow
| engineers to develop DSLs quickly, and to then verify
| properties in programs written using said DSLs.
|
| I can see some early signs of this trend in Idris, which is
| emphasizing DSL-building tools, or in smart contract projects,
| which are rushing to build contract languages with restricted
| semantics. There's also related work in Haskell and Racket /
| Scheme.
| exdsq wrote:
| I think realistically the biggest source of research money is
| from blockchain projects as so many use formal methods
| nowadays, and have done for a couple years
| sva_ wrote:
| It doesn't seem their formal methods are all that good for
| verification, looking at all the smart contract exploiting
| going on?
| exdsq wrote:
| Yeah for sure, but the underlying chains are pretty solid,
| and some of the languages are particularly well formalized
| such as Plutus (which is led by SPJ's son with a few of the
| original Haskell language team).
|
| But you can't save people from bugs higher up the stack
| when it comes to turing complete contracts. It can
| definitely be better though.
| [deleted]
| eschneider wrote:
| I hate to be that guy, but isn't the behavior for
|
| bool f(unsigned int x, unsigned int y) { return (x+y == y+x); }
|
| undefined when x+y or y=x overflow? So no, it's NOT guaranteed to
| never return false. :/
| sva_ wrote:
| Only if you assume x+y must be an unsigned int as well. They
| didn't specify the language, so you can't know that, I'd say.
| In a theorem prover you could prove this statement without
| doubt, but it's a bit weird they specified the unsigned int, to
| be fair.
| AdamH12113 wrote:
| Unsigned integer overflow is defined in C. Signed integer
| overflow is not, although in practice the CPU can do it just
| fine.
___________________________________________________________________
(page generated 2022-02-19 23:00 UTC)