mafribe

95 ms·

841.
by mafribe 11y ago
That's not really the essence of ROP because other attack techniques often also need to manipulate the stack. The key novel idea in ROP is to use data in unintended ways. This is based on the insight that the memory often contains shor
842.
by mafribe 11y ago
The paper introducing this concept is [1] but was long forgotten. Recently the use of derivations to implement regular expressions has become popular again, see e.g. [2]. [1] J. A. Brzozowski's, "Derivatives of Regular Expressions
843.
by mafribe 11y ago
You mean Goubault-style homotopy stuff. I don't this this is very categorical, e.g. [2] produces a single category, so I wouldn't call this an example of categorical structure. The Gunawardena paper [1] doesn't exhibit categ
844.
by mafribe 11y ago
I suspect that combining generics with subtyping might always lead you into the land on undecidable type-inference. After all, pure genericity (System F) is already undecidable.
845.
by mafribe 11y ago
What stops us is cost. Formally verifying non-trivial properties (in the sense of CompCert) with current technology is several orders of magnitude more expensive and time-consuming than programming and a bit of testing. And this price is al
846.
by mafribe 11y ago
imperative programming is not very interesting from a programming language theory point of view. I'm afraid I disagree, the opposite is the case. Modern PL theory is mostly about program correctness, and that is much easier
847.
by mafribe 11y ago
When I open Pierce TaPL and see immediately ML my heart sinks. I strongly recommend that you ignore this feeling and learn a modicum of ML coding. If you want to learn TAPL, just learn a bit of Ocaml. You don't need much. If y
848.
by mafribe 11y ago
I did point out the nesting and the requirement to name in C. The scoping follows immediately from beta-reduction (lambda x.M)N --> M[N/x] which I find very intuitive. I never had trouble understanding this, but maybe I&#x2
849.
by mafribe 11y ago
Show me the tutorial where I can build, _in C_ a bare bones working (tail recursion) implementation of the lambda calculus with type inference and dependent (algebraic?) types Why would you want to do that? Type inference and depe
850.
by mafribe 11y ago
I also don't think studying algebra helps you directly with programming language theory. However algebra is of indirect help if you want to learn category theory, because the latter is a direct generalisation of the former. It is rat
851.
by mafribe 11y ago
I think laziness-by-default is now mostly seen as a sub-optimal choice for general-purpose programming languages, and the complicated cost-model is one of the reasons. As far as I'm aware, even SPJ would agree with this (please correct
852.
by mafribe 11y ago
I agree with this. Given that Javascript is the undisputed king of browser languages, and the difficulties with Javascript as compilation target are becoming apparent, I expect that WebAssembly support will be something of a priority for br
853.
by mafribe 11y ago
Javascript has several disadvantages that make it less than ideal as a general compilation target. * Javascript is verbose because it's plain text and was 'optimised' for human readability, rather than machine-parsability. Th
854.
by mafribe 11y ago
This is true, but for some subjects you can partly get around this subject by doing a Batchelor at some free foreign university (and do really well there, like top of the year) and then doing a 1-year masters at expensive brand-name US univ
855.
by mafribe 11y ago
It's a useful technique not just for undergraduates. Here are two famous computer science examples. * Dana Scott discovered the lattice based model of the λ-calculus while trying to prove that no set theoretic models exist. This put fu
856.
by mafribe 11y ago
As so often in life, "follow the money"! Victimhood sells. The media loves to write about a damsel-in-distress, especially it the story sexually titillates, e.g. the UVA rape hoax or the Columbia U mattress-girl hoax. It sells cop
857.
by mafribe 11y ago
I don't think patch theory is untyped in principle. But all developments I've seen are untyped. And it's probably good this way, for typically you don't want to tie a version control system to a specific programming lang
858.
by mafribe 11y ago
The difference, I think, from patch theory is that Unison always preserves types while editing. Patch theory works with untyped text. The main result of [1], which Unison seems to be based on, is that you can form any well-typed term in the
859.
by mafribe 11y ago
As a lot of other commenters say, pattern matching, ADTs and higher-order functions are ideal for symbolic manipulation. Nowadays many languages have that (Scala, Rust, F#, Haskell), but Ocaml is old and was probably the first language that
860.
by mafribe 11y ago
It's questionable whether SAT solvers really work well for "the vast majority of the cases". They work very well for the problems they are tasked with. DPLL-based SAT solvers don't work well with randomly generated SAT i
861.
by mafribe 11y ago
Good. Session types are not the only approach to typing interaction, although probably the simplest.
862.
by mafribe 11y ago
I agree that it is good separate programming and verification. Otherwise the programmer is forced by the compiler to worry about correctness and termination from Day 1. Moreover, Cury-Howard based approaches really work only for a restrict
863.
by mafribe 11y ago
I'm not sure I can follow you here. What is ugly, Hoare logic? What does it mean to "build a whole language around Hoare logic"? What in your opinion are the alternatives to Hoare-style program logics that are general-purpose
864.
by mafribe 11y ago
Imperative, stateful computation [...] is [...] as [...] verifiable as pure-FP Exactly. When you verify your programs using some kind of program logic you realise that you have to keep track of all relevant data anyway. The condesc
865.
by mafribe 11y ago
Maybe the author plans to write about it in later parts of the article, but it's misleading to assume that (1) there is no work on types for interacting processes and (2) that types always have to be based on some underlying ideas form
866.
by mafribe 11y ago
There's a nice: do your undergraduate in Europe for free (and do well there), then do a Masters at your target US elite institution. Much cheaper, same brand recognition and Masters programs are a lot less selective, i.e. easier to get
867.
by mafribe 11y ago
Astir (αστήρ) means "star" in greek. I imagine that's where the G102 got its name from!
868.
by mafribe 11y ago
And I questioned why the OP made such a one-sided example, one that falls squarely in line with those who -- empirically -- disproportionally benefit financially from a divorce. I'm suggesting that the main concern should be the well-b
869.
by mafribe 11y ago
Are you not displaying sexist thinking here, in that you privilege mothers over fathers? Why should the well-being of the mother be the only relevant criterion? What about the well-being of the father and the children?
870.
by mafribe 11y ago
Why should a woman stay in an unhappy or abusive relationship? Turn this question around: why should a man stay in an unhappy or abusive relationship? Answer: because given the current divorce law, and, more importantly, divorce p

More ›