|
Boost : |
Subject: Re: [boost] [outcome] success-or-failure objects
From: Niall Douglas (s_sourceforge_at_[hidden])
Date: 2018-01-26 09:09:09
> Sure. I didn't mean to imply that just because some UB *might* be
> relatively benign that you should ever intentionally allow it to happen.
> Â We're talking about logic errors, where the call was made unintentionally.
Something really interesting for the future of C++ is that Outcome based
code which never throws exceptions is amenable to formal verification a
la CompCert for C. A few other things would also need to be dropped e.g.
virtual inheritance, RTTI, non-final virtual and so on. And only the
proposed freestanding standard library could be used
(https://github.com/ben-craig/freestanding_proposal/blob/eef741b6b1b8960e9e2e53d59df90e94872f7fb0/freestanding.pdf),
so most of the STL is not available.
But if you could tick those boxes, formal verification is within reach.
No idea who'd pay for CompCert to be extended to cover C++ though
(Airbus paid for CompCert to be created I believe).
Niall
-- ned Productions Limited Consulting http://www.nedproductions.biz/ http://ie.linkedin.com/in/nialldouglas/
Boost list run by bdawes at acm.org, gregod at cs.rpi.edu, cpdaniel at pacbell.net, john at johnmaddock.co.uk