xavxav

10 ms·

61.
by xavxav 3y ago
Based on the state of academic conferences in formal methods, I would have 4 languages: temporal logic, first order logic, concurrent separation logic and dependent type theory. This categorization provides generalizing powers because tools
62.
by xavxav 3y ago
This is a good list but is almost more accurately called a list of modeling languages. At the very least it’s a very particular interpretation of specification, which makes sense from a TLA+ expert but is incomplete. In particular I thin
63.
Specifying and Verifying Higher-Order Rust Iterators(hal.science)
4 points by xavxav 3y ago|0 comments
64.
by xavxav 4y ago
Yes that's what I meant, I'm curious if the Typst api would allow equivalents of those packages.
65.
by xavxav 4y ago
I was looking for a way to procrastinate on my thesis writing, maybe I'll convert it all to typst! More seriously, I am really following this project closely, and now that it's open source I'd like to see if its possible to a
66.
by xavxav 4y ago
My personal experience has shown me that static analysis of this kind does not scale for C, the complexity of showing just the memory safety of even simple programs grows astonishingly fast. Proof overhead for memory safety can frequently
67.
by xavxav 4y ago
not necessarily, depends on the embodied emissions in the replacement gear. It is also surprisingly hard to get any information on those. I tried seeing if there were estimates of the kg co2 in a modern CPU chip but I found nada
68.
by xavxav 4y ago
Great article, and I agree that Mutable Value semantics are an underused sweet spot in the semantic space. I’ve been watching Val from afar with great interest. I do think however that (safe) Rust can be said to have mutable value semantics
69.
by xavxav 4y ago
Simulink / Stateflow and more generally 'synchronous programming languages' have a rich academic lineage and are particularly well adapted to safety-critical tasks. These languages bring a lot of key guarantees that you can&#
70.
by xavxav 4y ago
> We already sent probe out of our Solar System. To give an idea of the scale involved, Voyager 1 is only 0.058% of the way to the nearest star system, and that took 45 years. Granted it wasn't built for speed but given that the
71.
by xavxav 4y ago
> Had DF monetized in 2006 instead of going free, and played the industry game as others do, I would not be surprised to see DF at $100M in 2023. I don't DF would have existed then, it would be hard to see it gather the same communi
72.
by xavxav 4y ago
Just checked your CV and it seems like the PDF version has several typos, specifically it says you are CTO at Meltwater when I think you meant at Pureskill.gg and is missing the entry for Seam :)
73.
by xavxav 4y ago
A half-serious thought I had is to allow AI to be trained on copyrighted materials but require all output to be public domain. It doesn’t solve attribution, and you could get a sufficiently advanced ai to “launder” copyright but at least it
74.
by xavxav 4y ago
I like the idea of specifying a parser through a formal grammar but I think that current technology has a few pretty annoying-severe flaws. * Parser generator grammars are usually quite far from 'paper' versions of a formal gr
75.
by xavxav 4y ago
I explicitly ignored codata/coinduction as they are complex and rather niche. Even so, they come with their own notion of 'termination' (progress / wfo) and don't magically let you write random non-terminating progr
76.
by xavxav 4y ago
Both, but almost more importantly the languages themselves are all strictly terminating. Long story short, these languages are based on the “Howard-Curry isomorphism” which says that we can view type signatures as theorems and programs with
77.
by xavxav 4y ago
I think this is what’s usually referred to as a “blackstart capacity”, and normally grid operators pay/ensure that certain operators maintain that capability. The issue is that I imagine that just keeping an idle natural gas generator
78.
by xavxav 4y ago
I know that this is a common wish, but anonymous sum types have pretty catastrophic impacts on type checking and lead to all sorts of bizarre corner cases like the following: let a = if cond { 1 } else { 1.0 }; a + 3
79.
by xavxav 4y ago
I don't a judge will care much about your argument that a sum is different from an average for patent infringement considerations.
80.
by xavxav 4y ago
For inlining in general, I think the wikipedia article is good https://en.wikipedia.org/wiki/Inline_expansion . The reason it's so important is that inlining synergises with other optimizations, its often run befor
81.
by xavxav 4y ago
While GATs are undeniably cool, I think I'm actually most excited by the enabling of MIR inlining. Rust level optimizations have a real potential to increase performance and decrease compilation times, and inlining is one of the most i
82.
by xavxav 4y ago
It's damning that there no truly functional grammar or spellchecker for latex, even ignoring crazy things that can be done with macros. If some billionaire wanted to 'move the needle' and change society for the better I think
83.
by xavxav 4y ago
I doubt it hurt performance, self-modifying code must play havoc on all the modern CPU caches, branch prediction, instruction decoding etc… A jit makes it worthwhile by doing it for hot paths for which the payoff outweighs this cost (or att
84.
Noether: Symmetry in Programming Language Design (2014) [pdf](github.com)
1 points by xavxav 4y ago|0 comments
85.
by xavxav 4y ago
The digital divide is a major problem today, and manifests all over the place, whether it’s spyware like this laptop, issues with phones or just interacting with service providers. I recently tried helping my aunt switch internet providers
86.
by xavxav 4y ago
> If I could, I would write in Sublime Text, because it's faster. However, no Sublime Text plugin for LaTeX exists. I'm using the Latex and LatexTools packagest, so I don't follow your point. It's pretty good and can
87.
by xavxav 4y ago
> The project is much more responsive to bug reports and code submissions than it has been in the past. Cool to see community listed as a feature up there with the tech stuff
88.
by xavxav 4y ago
M1 Pro === START OF SMART DATA SECTION === SMART overall-health self-assessment test result: PASSED SMART/Health Information (NVMe Log 0x02) Critical Warning: 0x00 Temperature: 28 C
89.
by xavxav 4y ago
Not really, it's more that I regularly make typos in all forms of writing (even handwritten). It's not usually misspellings but rather whole lexemes that go missing or are swapped. fwiw, I TA a course taught (partially) in OCaml a
90.
by xavxav 4y ago
I'll try to find an example of the syntax error I was mentioning, but I regularly trip up the parser with dumb mistakes which cause it to give completely useless errors. > Syntax errors are caught well by the parser which tells you

More ›