joomy

6 ms·

1.
by joomy 26d ago
Somehow the final version of the paper is not linked from the blog post: https://www.microsoft.com/en-us/research/publication/specifi...
2.
Why Rocq is better than Lean for program verification(joomy.korkutblech.com)
7 points by joomy 2mo ago|1 comments
3.
by joomy 2mo ago
A write-up on why I don't give in to the hype and switch to Lean for formal verification of programs.
4.
What Happens to Software When Proof Is Cheap? [video](youtube.com)
1 points by joomy 4mo ago|0 comments
5.
by joomy 7mo ago
The issue was a fun read, thanks for sharing.
6.
by joomy 8mo ago
Our 2 page extended abstract was more like a preannouncement. We hope to have a draft of the full paper by the end of the year. And we're not opposed to choice trees. I personally am not too familiar with them but there's time to
7.
by joomy 8mo ago
The title alone reads like the "digging for diamonds" meme.
8.
by joomy 8mo ago
We mean Haskell-style software transactional memory (STM). We call it a primitive because it is not defined in Rocq itself; instead, it is only exposed to the Rocq programmer through an interface.
9.
by joomy 8mo ago
I'm not entirely sure I fully agree with this definition; it seems somewhat arbitrary to me. Where is this definition from? My usual intuition is whether the generated code at the end needs a complicated runtime to replicate the source
10.
by joomy 8mo ago
> Have you considered combinatorial testing? Our plan was to do random Rocq program generation and differential testing of Crane extracted code versus other extraction methods and even CertiCoq. But fixing a program and trying different
11.
by joomy 8mo ago
This is another reason we are being careful with the correctness claim. The closest project I know right now that comes close to a formalized model of C++ is the BRiCk project: https://skylabsai.github.io/BRiCk/index.ht
12.
by joomy 8mo ago
Yes, we were careful not to call it that. I still don't mind calling our programs verified, since they are verified in Rocq and we do our best to preserve the semantics of them. Right now the only measure we have is testing a small s
13.
by joomy 8mo ago
Just like JavaScript folks like calling their compilers "transpiler", proof assistants folks like calling their compilers "extraction". Essentially it's a compiler from a high-level language to a slightly lower-leve
14.
by joomy 8mo ago
We do C++ only because C++ is the primary programming language at Bloomberg, and we aim to generate verified libraries that interact easily with the existing code. More about our design choices can be found here: https://bloomber
15.
by joomy 8mo ago
We're based in NYC. The Infrastructure and Security Research team in the CTO Office, in particular. And we are looking for senior researchers to join us, see https://x.com/jvanegue/status/2004593740472807498
16.
by joomy 8mo ago
Hi, I'm one of Crane's developers. You can map Rocq `bool`s to C++ `bool`, Rocq strings to C++ `std::string`s, etc. You just have to manually import the mapping module: https://github.com/bloomberg/crane/
17.
by joomy 8mo ago
You're right about the records providing flexible order, I overlooked that. But Kip lets you repeat cases in arguments, so you're not limited to 8 arguments for a function. In cases where a function takes multiple arguments of the
18.
by joomy 8mo ago
(bu tam-sayının) mutlak-değeri, (bunun 0'dan büyüklüğü) doğruysa, bu, değilse, bunun -1'le çarpımıdır. (5'in mutlak-değerini) yaz. (-5'in mutlak-değerini) yaz. You can try it in the playground.
19.
by joomy 8mo ago
Okay there is an updated web page and playground now: https://kip-dili.github.io/
20.
by joomy 8mo ago
Cases essentially act like named arguments, except the names are inferred from the case of an argument, which is inferred through morphological analysis. And that analysis can be ambiguous, so the ambiguities are solved by the type checker
21.
by joomy 8mo ago
"fark" here takes two arguments, the first (the minuend) is in instrumental case (-le), the second (the subtrahend) is in genitive case (-in). Now, because of the suffixes of the cases, regardless of the order in which you give th
22.
by joomy 8mo ago
Yes, that's one of my inspirations! I'm writing a short paper about Kip and I'm citing Perligata there for sure. The closest modern non-English programming language I know that also uses grammar features is Tampio, for Finnis
23.
by joomy 8mo ago
That's okay, thanks for sharing!
24.
by joomy 8mo ago
It would actually be a good fit for event handlers...
25.
by joomy 8mo ago
That's pretty cool! From what I can tell, it does a morphological guess based on the suffix. If you didn't have the apostrophe, it'd have issues with ambiguity (say "aşı", does it mean vaccine or does it mean "
26.
by joomy 8mo ago
Hi all, Kip's developer here! I was going to wait until we had finished the playground and landing page before posting about the project more, but here's the browser-based playground we have so far (thanks to Alperen Keles) for an
27.
Scraper for Twitter embedded timelines(github.com)
2 points by joomy 12y ago|0 comments
28.
A Haskell program to check the vezin (prosody) of Ottoman Divan poetry(github.com)
3 points by joomy 12y ago|0 comments