[HN Gopher] Show HN: FizzBee - Formal methods in Python
___________________________________________________________________
Show HN: FizzBee - Formal methods in Python
GitHub: https://www.github.com/fizzbee-io/FizzBee Traditionally,
formal methods are used only for highly mission critical systems to
validate the software will work as expected before it's built.
Recently, every major cloud vendor like AWS, Azure, Mongo DB,
confluent, elastic and so on use formal methods to validate their
design like the replication algorithm or various protocols doesn't
have a design bug. I used TLA+ for billing and usage based metering
applications. However, the current formal methods solutions like
TLA+, Alloy or P and so on are incredibly complex to learn and use,
that even in these companies only a few actually use. Now, instead
of using an unfamiliar complicated language, I built formal methods
model checker that just uses Python. That way, any software
engineer can quickly get started and use. I've also created an
online playground so you can try it without having to install on
your machine. In addition to model checking like TLA+/PlusCal,
Alloy, etc, FizzBee also has performance and probabilistic model
checking that be few other formal methods tool does. (PRISM for
example, but it's language is even more complicated to use) Please
let me know your feedback. Url: https://FizzBee.io Git:
https://www.github.com/fizzbee-io/FizzBee
Author : jayaprabhakar
Score : 110 points
Date : 2024-04-02 10:45 UTC (3 days ago)
(HTM) web link (fizzbee.io)
(TXT) w3m dump (fizzbee.io)
| knowsuchagency wrote:
| Very cool
| pkoird wrote:
| This is super cool! As someone who is interested but unfamiliar
| with formal verification, how "powerful" or "complete" would you
| say FizzBee is compared to the conventional tools such as TLA+?
| I'm unsure if I framed this correctly but can you do everything
| in Fizzbee that TLA+ supports?
| jayaprabhakar wrote:
| Yes, that's the intended goal. To do everything tla+ does
| (behavioral modeling) but not stop there. The second biggest
| area that's missing in tla+ but indispensable is _performance
| modeling_ that will be integrated. (PRISM model checker does
| it, but with a unwieldy complex language not suitable for more
| than a few dozen states) The performance modeling is work in
| progress, you can still try it, but you need to download and
| use the command line tool at present.
|
| The third goal is to make it suitable as a design documentation
| tool. I haven't started, but I would love to share the plan to
| get early feedback.
| User23 wrote:
| Does this generate executables like Dafny? Or is it more like
| TLA+ and focused on checking designs?
|
| What's it using on the backend for checking predicates?
| jayaprabhakar wrote:
| No, there's no code generation. In that sense, it's more like
| TLA+.
|
| The code generation is not in the plan, at least, not for the
| next couple of years until a few prerequisites happen that's
| not in my control.
|
| The primary reasons for not taking code generation are, 1. It
| complicates the model spec. My intention is, the spec should be
| as close to pseudo code as possible that is you ever write
| pseudo code on your design doc, it should be in fizz. 2. The
| past experience trying to do complete code generation all
| failed except for some trivial use cases (like protocol
| buffers)
|
| -- For the last question, for evaluating expressions, FizzBee
| uses starlark go library (subset of Python).
| sriram_malhar wrote:
| This looks fantastic. Can't wait to translate some non-trivial
| TLA+ to test it out.
| jayaprabhakar wrote:
| Thank you. Please let me know how it goes. Also, I can work
| with you on modeling it if you need - I'll want to see where
| the language design is causing the issue
| hwayne wrote:
| I'd also love to see what comes of this!
| westurner wrote:
| How does FizzBee compare to other formal methods tools for Python
| like Nagini, Deal-solver, Dafny?
| https://news.ycombinator.com/item?id=39139198
|
| https://news.ycombinator.com/item?id=36504073 :
|
| >>> _Can there still be side channel attacks in formally verified
| systems? Can e.g. TLA+ [or FizzBee] help with that at all?_
| jayaprabhakar wrote:
| FizzBee is an alternative to TLA+ designed to be the easiest to
| get started for every software engineer. To make it easiest to
| use, the language of specification is Python instead of using
| some kind of mathematical presentation language like TLA+. So
| it's a formal methods in Python not for Python.
|
| FizzBee is a design specification language whereas Nagini and
| deal solver are implementation verification language. FizzBee
| is supposed to be before you start coding, or actually before
| sending out the design document for review to iron out design
| bugs. The latter two are supposed to be used to verify the
| implementation.
|
| Dafny is actually an implementation language designed as
| verification aware programming language. It does code
| generation into multiple languages and inserts various
| preconditions and other assertions into the code. Again, it is
| suitable for verifying the design.
| westurner wrote:
| Is it advantageous to maintain separation between formal
| design, formal implementation, and formal verification formal
| methods?
|
| Is there still a place for implementation language agnostic
| tools for formal methods?
|
| icontract and pycontracts do runtime type checking and value
| constraints with DbC Design-by-Contract patterns that more
| clearly separate the preconditions and postconditions from
| the command, per Hoare logic. Both can read Python type
| annotations and apply them at runtime or not, both support
| runtime checking of invariants: values that shouldn't have
| changed when postconditions are evaluated after the function
| returns, but could have due to e.g. parallelism and
| concurrency and (network I/O) latency and pass by reference
| in distributed systems.
| johndough wrote:
| I was looking for Python code, but did not find anything, until I
| realized that it said "Python-like" instead of "Python" on the
| website. I'd suggest to change the title to reflect that. I did
| not recognize the *.fizz files as Python.
| jayaprabhakar wrote:
| I agree, the body of the action and functions are Python,
| actually starlark (a subset of python). I'll update the
| description.
| atomicnature wrote:
| I think one of Lamport's arguments was that at specification
| level one shouldn't go for an imperative approach. Imperative is
| good for "how to" instructions (programs). Declarative is good
| for "what is" or "what should be" instructions (specifications).
| So in that sense TLA+ was about helping you build state machines
| via simple declarative syntax. Of course this was Lamport's
| argument, in practice, your approach may work just as well. Will
| definitely be interested to see how your approach evolves.
| erezsh wrote:
| I like the idea of being able to use this in a real program, but
| I'm not sure how that would look. I browsed the docs, and I
| didn't see it addressed. I guess the question boils down to - how
| would it interface with other languages? On its own, it can't be
| used for general programming, so the only option I can think of
| is to run it as a DSL interface to a general programming
| language. Probably Python, since it's the easiest in this case.
| But it's not obvious to me what that API would look like, or what
| would be the right way to use it. Do you have any thoughts on
| this subject?
___________________________________________________________________
(page generated 2024-04-05 23:02 UTC)