oggy

5 ms·

1.
by oggy 7mo ago
I'm not a mathematician either ;) Yeah, I won't sit around and ponder at a property definition for weeks. But I will maybe spend a day on it, not get anywhere, and then spend an hour or two a day thinking about ways to formulate i
2.
by oggy 7mo ago
In my experience, finding the "correct" specification for a problem is usually very difficult for realistic systems. Generally it's unlikely that you'll be able to specify ALL the relevant properties formally. I think th
3.
by oggy 11mo ago
I see, so it unifies type (or I suppose term in this case?) erasure and linear typing? Thanks for the explanation!
4.
by oggy 11mo ago
I haven't followed closely, and I'm only faintly acquainted with algebraic geometry and category theory. But the TFA links to a formalization of Grothendieck schemes, which are definitely post-WW2 material, and they rely on the Is
5.
by oggy 11mo ago
Thank you for spelling this out; comments like these make this website worthwhile. You've enlightened at least one person today. You hinted that there's more to QTT (or its implementation in Idris?) than this. Could you elaborate
6.
by oggy 1y ago
Thank you for the kind words! I haven't really talked about it anywhere yet since it's fresh off the press, I'll definitely post it on the mailing list.
7.
by oggy 1y ago
I think the main answer was given by another comment: for most projects, correctness usually isn't worth that much (i.e., a bug isn't that expensive for a company producing a piece of software). It also isn't in the software
8.
by oggy 1y ago
Funny to see this posted on HN, just last week I finished writing a blog post about a project I did for checking that code matches the TLA+ specs so I have to shamelessly plug it :) [1] I was aware of the MongoDB paper, but I ended up actua
9.
by oggy 2y ago
A funny anecdote from a concert a few years ago: Allen was playing a solo, holding a note and blowing as hard as he could on his little soprano sax. Next thing you his teeth fly out, and there's a general commotion on as the rest of th
10.
by oggy 2y ago
Maybe not range per se, but there are a couple of Europe-specific things that make EVs less attractive. First, many people live in apartment buildings and park their cars on the street, with no charging facilities. So they'd have to ma
11.
by oggy 2y ago
TLA+ has also had an SMT-based backend, Apalache [1], for a few years now. In general, you encode your system model (which would be the Rust functions for Verus, the TLA model for Apalache) and your desired properties into an SMT formula, a
12.
by oggy 2y ago
"Verifying" and "proving" are synonymous in this case. You prove or verify that the system satisfies some specification, i.e., properties. Your normally write the properties yourself, but sometimes the properties are har
13.
by oggy 3y ago
Great to see this. I hope it takes off - Bazel is useful but I really like the principled approach behind it (see the Build Systems a la Carte paper), and Neil is scarily good from my experience of working with him so I'd expect that t
14.
by oggy 4y ago
FWIW, I have a PhD in formal methods and spent a good chunk of that PhD proving stuff about distributed systems in Isabelle. I'm vaguely familiar with Coq. At work I've been largely using TLA+ the last few months to analyze design
15.
by oggy 4y ago
Thanks for your work, Hilel! I've been using TLA extensively in my job the last few months (I work at a blockchain company), and it's been a good run - we found a bunch of issues in several designs and even implemented code (some
16.
by oggy 4y ago
I used Spin a few years back, so my memory is a bit hazy, but I remember Promela (Spin's modeling language) feeling extremely low-level in comparison. It felt a bit like more limited C with non-deterministic choice stuck in there. TLA
17.
by oggy 5y ago
I bought a Remarkable 2 for note taking and annotating scientific papers. As far as it's promise of "better paper", I think it's only partly fulfilled. I haven't returned it, but I'm sadly also not using it reg
18.
by oggy 6y ago
The idea is not to replace every banking system, but to create a network with a sufficient technological edge over existing solution and sufficient business value. CHESS is definitely a complex beast. The go-live date has moved from 2021 to
19.
by oggy 6y ago
I don't have a financial services background myself, so assessing I can't really comment on the risk of consolidating custodianship and trading. But market consolidation will at some point run into legal and jurisdictional limits
20.
by oggy 6y ago
Shameless plug: the problems that you describe are almost exactly what we're trying to solve with DAML and Canton [1]. From the Canton whitepaper: Building distributed applications that involve multiple organizations is hard with today
21.
by oggy 6y ago
AI can be very useful in practice for theorem proving WITHOUT proving "big new theorems" or inventing new mathematics. Right now, what makes theorem proving an extremely expensive undertaking is making proof search work. AI could
22.
by oggy 6y ago
Sorbillo's is the best I've tried. I remember walking in front of the shop a few times and thinking it's some kind of tourist trap (it's on the possibly most touristy street in the city), but decided to try it out in the
23.
by oggy 6y ago
Yeah, like I said I don't know what the current available supply is, which IIUC is the more limiting factor. I also don't know what the current prices are, and I don't know which part of it are production costs and which par
24.
by oggy 6y ago
Before the outbreak, N-95 masks used to cost 58 cents. So if it was spent on masks only, around 1.7 million masks at those prices. I don't know how many health workers SF has, but at a population of 800k and a US average of 2.6 physici
25.
by oggy 6y ago
I've attended several short courses on giving presentations. This one by an ETH Zurich professor is the best one I know of: https://inf.ethz.ch/personal/markusp/teaching/guides/guide-p... He has a l
26.
by oggy 6y ago
Great comment about missing the forest from the trees. The course outline reminds me of an article on "writing great code" that lists the rules of a code formatter. My personal tips for writing docs: 1. think about what you need t
27.
by oggy 6y ago
Your dismissive tone is uncalled for and not appreciated. Here's a systematic review that cites several studies that find face masks show a statistically significant effect in protection against influenza: https://www.bmj.co
28.
by oggy 6y ago
Feedback on the website: it's running quite slow for me on Chromium under Linux, especially if there are a lot of locations (for example, unchecking "exclude public health agencies" makes the site very unresponsive). Also, &q
29.
by oggy 6y ago
Thank you for the work on this. I have a tangentially related question, hoping that someone knowledgeable can answer. What are the main bottlenecks to scaling testing, in particular in the following stages: - the supply of virus-specific re
30.
by oggy 6y ago
Interesting, this is the first time I hear that touching fomites is the primary vector of spreading. The CDC page says the opposite: https://www.cdc.gov/coronavirus/2019-ncov/prepare/transmissi... But I do ap

More ›