nextos

7 ms·

91.
by nextos 7mo ago
Lean and Coq might not be the right choice. Perhaps something like Dafny, F*, or Why3, where code and theorems live together. Nevertheless, Lean 4 has closed the gap and it's closer to those than Coq at this stage.
92.
by nextos 7mo ago
Not surprising, as Dafny is a bit less expressive (refinement instead of dependent types) and therefore easier to write. IMHO, it hits a very nice sweet spot. The disadvantage of Dafny is the lack of manual tactics to prove things when SAT&
93.
by nextos 7mo ago
Formal specifications can be easier to write than code. Take refinement types in Dafny, for example. Because they are higher-level, you don't need to bother with tedious implementation details. By shifting our focus to formal specifica
94.
Agents of Chaos(arxiv.org)
3 points by nextos 7mo ago|0 comments
95.
by nextos 8mo ago
There are incomplete parsers that cover most of the Org basics. For example, GitHub has one, crafted in Ruby. They use it to render e.g. readme.org files in repositories. It works quite well. I find the Org format very pleasant to work with
96.
by nextos 8mo ago
There are many classical theorem provers that use simple type systems, e.g. Isabelle. Mizar is even weakly typed.
97.
by nextos 8mo ago
As a heavy user of formal methods, I think refinement types, instead of theorem proving with Lean or Isabelle, is both easier and more amenable to automation that doesn't get into these pitfalls. It's less powerful, but easier to
98.
by nextos 8mo ago
In EU/UK, some are sadly app only. I avoid those. Many others are pushing apps as a 2FA, even if you use their website. You need to insist to get another authentication system, like TAN. Some governments are also pushing mobile IDs. Th
99.
by nextos 8mo ago
If verification is the goal, but you don't want to learn theorem proving yet, Dafny is really approachable and practical [1]. F* is also worth considering as a proof-oriented alternative to Isabelle that is focused on software verifica
100.
by nextos 8mo ago
Lean is great, but if someone's primary interest is SWE, I think there are better choices. The Lean community is primarily focused on formalizing mathematics right now. This might change in the future. Lean is nice to learn theorem pro
101.
by nextos 8mo ago
Is it less glamorous? As an academic, my impression is that lots of innovation is now done at industrial labs. In general, Academia lacks sufficient resources and appropriate structures for dedicated efforts. Pay is abysmal and politics is
102.
by nextos 8mo ago
AFAIK, the classic Toyota Land Cruiser (J70) has not been sold in EU for more than a decade since it doesn't comply with emission regulations. Interestingly, some are assembled in Portugal for North African and Middle East markets.
103.
by nextos 8mo ago
Lobsters and filter posts with vibecoding tag.
104.
Agentic Proof-Oriented Programming(risemsr.github.io)
1 points by nextos 8mo ago|0 comments
105.
by nextos 8mo ago
Progress with RL is very interesting, but it's still too inefficient. Current models do OK on simple boring linear code. But they output complete nonsense when presented with some compact but mildly complex code, e.g. a NumPyro model w
106.
by nextos 8mo ago
Snap and Flatpak do both sandboxing and package management. You can use the underlying sandboxing with bwrap. A good alternative is firejail. They are quite easy to use. I prefer to centralize package management to my distro, but I value th
107.
by nextos 8mo ago
I really like everything Uri Alon (last author) publishes, but these types of studies have a history of inflating genetic contributions to phenotypes. Decoupling genetics from environment is not easy as they are both highly correlated. In f
108.
by nextos 8mo ago
I agree. I think fixing the keylogging issue should be possible without dumping the entire architecture. Perhaps the new X11 fork https://x11libre.net will achieve that? At least, it's encouraging to hear it's getting
109.
by nextos 8mo ago
Defense in depth. One compromised application may do a lot of harm if it has access to your keyboard inputs. Supply chain attacks are not that uncommon. While you can trust software developers, you cannot completely trust their builds.
110.
by nextos 8mo ago
I prefer X11 as well, but it has some security issues. Notably, all applications can read your input at any time. It's really hard to sandbox. Wayland brought some irritations, including increased latency, and an architecture that requ
111.
by nextos 8mo ago
Deep SSMs, including the entire S4 to Mamba saga, are a very interesting alternative to transformers. In some of my genomics use cases, Mamba has been easier to train and scale over large context windows, compared to transformers.
112.
by nextos 8mo ago
True, but Google Translate was already "AI". They previously used LSTMs. And before LSTMs, it was ML-like statistical translation.
113.
by nextos 8mo ago
> [...] the same in the sense that they are just as poor in quality? I mean some real-time software for critical embedded systems has an incredible level of rigor, making heavy use of static analysis, model checking, and theorem proving.
114.
by nextos 8mo ago
Maybe formal methods have a chance of becoming mainstream now [1]? This would increase the rigor of software engineering and put it on par with civil engineering. Some niches like real-time embedded systems are already pretty much the same.
115.
by nextos 9mo ago
Medicaid holds previous addresses, household details, previous diagnoses, ethnicity, etc. It is quite trivial to infer if someone is likely to have emigrated to the US due to obvious gaps in records or in their relatives' ones. This is
116.
by nextos 9mo ago
Their local Palantir implementation is called POL-INTEL. This thesis presents a good critical overview [1]. [1] https://en.itu.dk/-/media/EN/Research/PhD-Programme/PhD-defe...
117.
by nextos 9mo ago
The framework is the one I referred to (EU LED). In Denmark, LED is implemented in the Danish Law Enforcement Act. However, LED has some purpose limitations, which critics argue the Danish Law Enforcement Act has bypassed. Some are trying t
118.
by nextos 9mo ago
Ironically, the Danish Government is a heavy user of Palantir systems, including creepy predictive policing solutions. I would be keen to know if citizen data is being handled correctly, following GDPR/LED. Given previous Danish client
119.
by nextos 9mo ago
I wouldn't use snap or Flatpak, just sandbox using bwrap or firejail. They are really easy to use. Containers also provide good development sandboxing. With distrobox you can run many distributions inside your own within a clean and is
120.
by nextos 9mo ago
Linux comes in a wide range of distributions, so it is hard to make universal claims. One area where security defaults need to improve is sandboxing. If security is a major concern, bwrap or firejail can easily provide that extra sandboxing

More ›