Threads for MichaelBurge
-
re related topic
“A good smart contract language is a $1 billion problem. Why? Look at the amounts lost in some recent hacks:”
Why aren’t more of them just trying SPARK Ada if it’s so costly to fail and they need a language? I’ve never understood this. Let’s say it’s $3000 a license. That’s probably high but on purpose. They’re pulling in millions to a billion dollars. Any coding errors can loose that. SPARK gets them immunity to most coding errors plus easier proof of their contracts. Using a constrained, functional style makes that even easier. They get this assurance for a few grand. The increased use of SPARK for smart contracts makes AdaCore and CompSci start developing all kinds of libraries and theories that increase automation in those kind of works. Other projects outside SPARK, including FOSS, will follow suite to match it.
Don’t get me wrong: I find all this work really interesting. I even expect new stuff to be developed in parallel with using proven stuff. That the cryptocurrencies are also bringing mainstream audience into formal methods is neat, too, since how else is that going to happen [1]? ;) It’s just strange that most are avoiding tools proven to do the job to try prototype tools when there’s so much risk. At the least, I’d expect people to default on things like SPARK until alternatives mature and have many successes under their belt.
[1] Hopefully @hwayne’s TLA+ book if nothing else outside of cryptocurrencies. I’m really hoping and betting on that one given so many startups are doing distributed systems needing a way to bulletproof them faster and cheaper.
re your article
Your work on Pyramid looks really good. You made it small, useful, and have testing/model-checking by default. Probably all wise decisions given target audience. Presented in a clear, accessible way. Great stuff. :)
I especially liked that you tied it to Beautiful Racket. Reason is that I was looking at it just a few days ago when it got posted to Hacker News for similar purpose: a C-like language oriented toward verification and metaprogramming. Although putting the project off for months, I keep coming back to the idea of Racket tying the style to books like HtDP, SICP, and/or Beautiful Racket for onboarding new contributors more easily. They get to learn Scheme, metaprogramming, an IDE for both, and a step into highly-robust code in one, smooth flow. Whereas, outside of Racket or done in separate languages, the higher barrier to entry might force them to learn less since they have to pick and choose.
So, the language gets Racket’s tooling/IDE, it’s easier to build, they get benefit of learning Racket, and they get to learn the verification-oriented language in it. What you think on those potential advantages of Racket for high-assurance languages? It looks like you’re doing something similar but you might have some other reasons.
-
Thanks for reading, Nick.
One problem there is that Ethereum has a custom instruction set, so no existing languages can compile to it. That leaves Solidity as the only option.
Cardano are using a formally-specified variant of LLVM. Since there is an Ada for LLVM, it should be possible to use Ada to program Cardano contracts when they release it in the next few weeks.
Some Ethereum people want to use WebAssembly for the next version of its VM. People mainly interact with Ethereum applications via websites and the Metamask browser extension, so this lets them share code between their websites and the contracts. I’m skeptical myself.
Ethereum contracts are vulnerable to a different class of bugs than ordinary software, so most people’s suggestions for “improving” security are targeting the wrong issues. I see that SPARK purports to support bounds on space and time. That actually makes it far better than most suggestions, since this is a crucial security requirement in Ethereum.
For example, the DAO issue was a “re-entrancy” attack, where the same contract is run multiple times within the same transaction. Protecting against this requires all state-modifying code to be idempotent.
I like your idea of writing a high-assurance language in Racket. I’m considering picking up the PLT Redex book[1] myself. Writing my C compiler has made me think that every standardized language should have a formal semantics:
C:
int x = sizeof(x++);Lisp IR:
(define x (allocate-local *platform-native-size*)) (write-local x (type-size (expression-type (+ x 1))))The C++ standard would be much shorter if it came with a precise Lisp dialect. And a verification language seems like it needs a clear semantics to know what exactly it’s verifying.
[1] https://mitpress.mit.edu/books/semantics-engineering-plt-redex
-
re SPARK/EVM
Yeah, SPARK was meant for real-time applications with space and memory bounds. So, I figured there should be overlap in what it does and Ethereum needs. Good news on Cardano having a potential tie-in to Ada via LLVM.
Far as using SPARK, I knew the EVM used its own instruction set. My concept was more modeling those operations in SPARK similar to how many have done with typed x86 or abstract machines. You essentially make a state machine for EVM in SPARK that lets you verify EVM assebly. Then, you model your contract in high-level SPARK that’s close to the machine. After proving those properties, you do a hand- or tool-based translation to EVM modeled in SPARK. If the contract is simple, then the assembly equivalence might be straight-forward to check by eye (caveat: I don’t know EVM). Reduces need for trusted compiler. The properties of the contract are then proven on the simulated assembly in SPARK. That’s extracted by hand or tool into actual EVM again checked by eye since they should look about the same.
You’re actually stronger in formal verification than me since you actually do it vs read about it. Haha. So, I’m curious how effective you think that might be. There’s prior art but each project is different. Outside SPARK, the TALC and X86.Proved projects give me hope these simpler assemblies could be tackled with approachable tooling.
re Racket
Yeah, I agree on semantics formally or in LISP for new languages. It’s a good check on complexity. Btw, one of the works I plan to draw on is ZL which essentially is C++ in Scheme. I imagine the two people it took to do that with C compatibility was less work than it would take (did take) to do it in C or C++ themselves. I’m just speculating as a guy who has seen productivity studies on LISP vs C/C++… ;)
PLT Redex looks good. Thanks for the tip. Bookmarking it. Far as blockchain VM’s, one more work that you’ve probably seen but just giving it to you in case you haven’t. It’s about a newer one while also referencing their EVM work. Rosu’s group seem to be the most productive on formally specifying languages that, via their K Framework, automatically get some useful tooling. That C Semantics is still jaw dropping work to me given how many barely-functional attempts I’ve read over the years at modeling things like mini-Pascals or partial versions of C. They usually had no tooling, too. Building these languages on Racket, K Framework, or preferably both is a substantial improvement to where high-assurance languages were at just five years ago.
-
WebAssembly is just a well-specified VM to do computation. I too am skeptical about code sharing argument, but it seems to me WebAssembly is clearly superior to LLVM, which was designed as a compiler IR and very much not designed as a portable assembly. What’s your main problems with WebAssembly?
-
-
-
Pretty neat. The other nearly-universal technique is to attach gdb to the process, and repeatedly stop ask for a backtrace. Works with many interpreted languages like Python or Perl, SQL, C, etc. If you collect 5-10 samples, that’s enough to start with.
And strace is a quick way to see if it’s blocked on a system call or e.g. repeatedly opening the same file.
-
-
The gdb technique even has a website: http://poormansprofiler.org/ =D
( https://gist.github.com/unhammer/4e91821075c2485999eb has some handy tweaks on that for OCaml programs)
-
-
The ability to show descendents of a check-in.
Both Git and Fossil can easily find the ancestors of a check-in. But only Fossil shows the descendents. (It is possible to find the descendents of a check-in in Git using the log, but that is sufficiently difficult that nobody ever actually does it.)
I use commit ranges to diff everything I’ve done since a commit, or browse its descendants.
git log release-v3.8.. -
-
If you want to check out a practical gradually-typed language, I’ve been using Typed Racket.
It’s very convenient to use untyped code early-on when the design of the program is unclear(or when porting code from a different language), and to switch individual modules to typed code later to reduce bugs.
-
-
-
Based on reading https://docs.perl6.org/type/Cool, kinda? Although it also looks to me as if this is at once broader than what Perl 5 does (e.g.
123.substr(1, 2), or howArrayis also aCooltype) and also a bit more formal, typing-wise, since each of those invocations makes clear that it needs aCoolin itsNumericorStringform, for example.-
That makes sense that it changed. perl5 is not so.. structured. But this stuff worked:
"4" + "6.2" $q=42; print "foo$q" print "foo" + $qIt makes things like numeric fields in HTML forms very easy (
if $form["age"] <= 16), but the subtle bugs you get…Anyway. That was perl5. The perl6 solution seems to make things much more explicit.
-
-
-
-
stanza is another interesting language that is designed from the start to be gradually typed.
-
Typed Racket is indeed an awesome example. I believe TypeScript would also qualify very well here (as might Flow; I’m not as familiar with it). This also reminds me of Dylan of yore, too: https://en.wikipedia.org/wiki/Dylan_(programming_language)
-
Is this the same thing? I had the same thought and I wasn’t sure if it was.
-
-
-
Usually the Haskell people will define the types, and then have the compiler generate the serialization code. See the Serialization part of my article:
http://www.michaelburge.us/2017/08/17/rolling-your-own-blockchain.html
Why use ADTs rather than e.g. S-expressions or JSON? Because it lets you fully-resolve ambiguity earlier rather than later. If the data you’re parsing is from a web service, that may not be important - they might be generating it from an XSD with rigid typing. Machines often don’t emit ambiguous data.
But if the data you’re parsing is e.g. source code that a user wrote, it’s better to go from parse tree to ADT early on. Anything near humans needs an ADT.
-
You might want to move the disclaimer to the top of the page, for your own legal protection, just in case the satire’s a bit too subtle for someone.
-
I agree to refund anyone who purchases a Basilisk Protection Charm yet ends up tormented for all eternity by a rogue AGI.
Hopefully that warranty avoids the need for any lawsuits.
-
-
Do you believe @MichaelBurge will be sued by someone who believes in the Basilisk?
Or by angry cryptocoin investors?
-
-
MichaelBurge
edited
5 years ago
|
link
| on:
This Interview Was Conducted on an Anonymous, DIY Cell Phone Network
I like the idea of a decentralized wireless internet. Who cares what Comcast is doing with Net Neutrality when people can set up their own Last Mile Network. You still need fiber for inter-city connects, but that’s a lot cheaper than digging up all the streets in every city.
How feasible is such a decentralized internet? Isn’t the existing internet vulnerable to malicious BGP updates? Could you charge for internet traffic running through your node(with e.g. Bitcoin), to incentivize people setting up new wireless nodes?
In Portland, there’s an ISP using wireless radio towers. I don’t know if it’s similar to the wireless cell phone networks: https://www.stephouse.net/
-
Ideally, I think something like a crowd funded version of project loon would be great for connectivity at scale. These could be nodes that connect mesh networks across cities and countries.
-
Who cares what Comcast is doing with Net Neutrality when people can set up their own Last Mile Network.
net neutrality is still important; without it ISPs could still block/throttle sites for everyone not using the decentralizes/alternative ISP. it would still limit the reach of people who refuse to pay the centralized ISPs.
-
-
i would like to believe that, but it hasn’t happened in similar situations in the past. there was no mass exodus from gchat when they canceled XMPP support, for example. so in addition to net neutrality regulation we need regulations to enforce open standards (i.e. gchat and facebook messenger should be required to support XMPP or some other open protocol). the market hasn’t worked.
-
there was no mass exodus from gchat when they canceled XMPP support, for example
That’s not an apples-to-apples comparison though, is it? If ISPs make life difficult enough, and decentralized alternatives exist and are viable, then people will adopt the alternatives.
so in addition to net neutrality regulation we need regulations to enforce open standards
Nope, we don’t need government coercion to fix problems caused by government coercion. The problem can’t be its own solution.
I’ve even seen someone say that “net neutrality” is/was a bad thing because it limits competition. I don’t know if that’s accurate in this case, but as a general rule of thumb, actual competition is always a good thing.
-
That’s not an apples-to-apples comparison though, is it? If ISPs make life difficult enough, and decentralized alternatives exist and are viable, then people will adopt the alternatives.
ISPs can ruin the internet without making life difficult for 99% of people. They could limit/throttle access to sites in such a way that the number of people who are affected day-to-day is comparable to the number of people who were affected when gchat removed XMPP support.
Nope, we don’t need government coercion to fix problems caused by government coercion. The problem can’t be its own solution.
How is the industry’s departure from open standards caused by government coercion?
-
I’d like to see stats on competition limiting. It’s true that in a healthy competitive environment, net neutrality laws would be less needed, but telecom always trends to very little competition when left alone
-
telecom always trends to very little competition when left alone
But it’s not left alone! That’s what I’ve been repeating here.
Every country on earth has a state-maintained cartel of ISPs, i.e. the government prevents any real competition from bothering their buddies running the ISPs.
That’s why you’d need a license to even try and start an ISP, right? The license will be expensive, and if you seem like you’d actually compete on quality and price, then you just won’t get it no matter how much money you have.
Or if you manage to get going, and start being a nuisance by providing people with a good connection for a good price, then you’ll be shut down by the government. It doesn’t need to be like, they show up and tell you to stop competing, they can just bury you in bullshit paperwork until you quit.
-
That’s why you’d need a license to even try and start an ISP, right?
If they started requiring licenses to run an ISP here I could see people getting very upset about that.
-
-
-
-
-
-
-
-
I think piracy shows that it’s pretty hard to control technology in practice. You can pass all kinds of regulations, but you have to be able to enforce them as well for them to have teeth. When technology is cheap and ubiquitous people will use it, and there’s not much you can do about that.
-
Piracy showed it was hard for entertainment industry to control what ISP’s and their users were doing when ISP’s didn’t want to spend their own time and money enforcing entertainment industry’s will. That tells you nothing about what would happen if ISP’s paying off Congress wanted something done to benefit ISP’s. The recent FCC ruling tell us they get results they want when their people are in office. So, they’d get what they wanted there, too.
-
-
-
-
-
The choice of name is hilarious.
-
I particularly like that it is a implemented in Racket….
I’m sure he can create some extensions like a Madoff package manager and a Ponzi operator and….
-
-
-
The cover is even better: https://twitter.com/TaurineAndCode/status/936293090440110081
-
-
Totally brilliant. Combined with Racket, the name might be unbeatable.
-
-
They probably should’ve used a “Formula CSV”(.fcsv, or .fsv) file extension that extends “Data CSV”(.csv) with arbitrary formulas. Or even a “Program CSV”(.pcsv, or .psv) for network requests or shell commands, though that one might be too many choices of file format.
I also like the converse: If you’re writing a program, use a programming language!
The contrapositive is even better. If you are not using a programming language then you are not writing a program.
I think you flipped an “ought” to an “is” when you took the contrapositive.
Is my language incorrect?
Okay will this then be more clear?
If not using prog. Lang. => not writing program
The original statements say how things ought to be, your statements are about how the world is. The proper contrapositive would be
“if you aren’t using a programming language, it isn’t true that you should be writing a program.”“if it’s not the case that you should be using a programming language, you aren’t writing a program.”Not true for what most people think of as “programming languages” (or, if you prefer, many programming languages are not obviously so).