Reach’s big claim to fame (other than that they’re endeavoring to be a cross-platform blockchain solution) is that their compiler does a great deal of theorem-proving, in order to avoid producing anything that could cause tokens to vanish irretrievably into a proverbial black hole.
Are there any similar failsafes for PyTeal, Beaker, or AlgoKit?
Also, does anybody know anything about using Reach-generated TEAL with dappflow?
(Note that the last time I did anything with Reach, it was the Trust Fund workshop, and for some reason, it was categorically refusing to behave “as advertised,” at least running on an Algorand DevNet, with the trial that theoretically should return the “Monopoly-Algos” to the Funder instead giving them to the “Bystander.” Not just for me, but for others, and not just for my solution but for the canned solution, and nobody seemed to be in any hurry to do anything about it. And one look at the TEAL code put me into “deer in headlights” mode.)
Well first of all, it’s not just PyTeal, Beaker or AlgoKit. There’s also, Tealish, TealScript, CEAL and there are strange rumours and rumblings of some skunkworks project connected to MS technology here : Algorand for Visual Studio - YouTube The latter prospect being truly frightening as it could mean, for example, that they could mandate login to Windows with Algo wallet only ;-). If that doesn’t drive mainstream adoption, I have no idea what will.
In any case, to answer your question there is KAVM. This is a formal verification engine based on K. At least, I think that answers your question.
What’s “K”? Other than the letter after “J,” and the character Tommy Lee Jones played in the Men in Black movies? (For pity’s sake, why can’t people give development tools names that are easy to search for on Google and Wikipedia? Like RPG [before it became a game genre, it was Report Program Generator], PL/I, APL, FORTRAN, COBOL. They were all distinctive words that didn’t mean anything else, long before there was such a thing as a search engine!)
It is a language for describing languages. It was used to model the AVM. This model is then used by something called the Z3 engine to solve assertions made during static analysis. For example you could make static analyses of TEAL contracts to prove that certain conditions could never happen, like an input being too high, or a security vulnerability ever appearing. This is all quite new Algorand functionality but missing the media radar. I think Algorand wants to fly under it IMHO
If you look at KAVM you can use it in SCs now. The idea is I think it saves you a fortune on audits. I am not sure if it is past beta today or no though
We’re glad to announce the public beta release of KAVM, a formal semantics of the Algorand Virtual Machine powered by the K Framework! This work was funded by @AlgoFoundation through their developer infrastructure grant program https://t.co/GsCXfNmhRA Blog by @georgy_lukyanov” / Twitter