Bayle Shanks's website: proj-oot-ootNotes19

for soft-realtime, eg audio, can't block. So ppl want to avoid garbage-collected languages [1]. One guy says Go can work, but is a pain, and that Rust would probably be better.

---

this guy's tips for soft-realtime audio:

" These mistakes basically boil down to not using slow scripting languages and making the core buffer loop run fast and undisturbed. For realtime synthesis use c or c++, optimise early, use trigonometry approximations in range -pi / pi, do not use lookup tables, they unnecessarily fill the cache, cpus are fast enough, write the core loop branchless, write for cache, use vectorisation and function pointers. Do not use anything fancy, simple int32_t, float and vector/array is enough (some filters need double precision though). Do not copy stuff, point to it. Precalculate what can be precalculated, e.g. dont do x / samplerate, do x * samplerate_inverse. Check for denormals. ... You should not use standard pow and log but approximations of these functions. These are usually faster than any lookup table that fills a good part of the cache and then you stall. But there might be some gray area, depending on the system. Or when full precision is needed. In most audio cases approximations work very well. Atleast that was what my testing showed.

edit: it might be different for a single plugin, where there isn't much need for cache, but as the core loop grows bigger, you also need the cache more. "

---

Five cooperative functions trampolining on a thread One called I/O and blocked that thread Mama called the doctor and the doctor said: "No more blocking on this thread!"

-- me

true story bruh

---

the conclusion of http://hackingdistributed.com/2016/06/18/analysis-of-the-dao-exploit/ struck a chord with me:

" I think the susceptibility of 1.1 to this attack is really interesting: even though withdrawReward for was not vulnerable by itself, and even though splitDAO was not vulnerable without withdrawRewardFor, the combination proves deadly. This is probably why this exploit was missed in review so many times by so many different people: reviewers tend to review functions one at a time, and assume that calls to secure subroutines will operate securely and as intended.

In the case of Ethereum, even secure functions that involve sending funds could render your original function as vulnerable to reentrancy. Whether they're functions from the default Solidity libraries or functions that you wrote yourself with security in mind. Special care is required in reviews of Ethereum code to make sure that any functions moving value occur after any state updates whatsoever, otherwise these state values will be necessarily vulnerable to reentrancy. "

in other words, programming with reentrancy requires a sort of red function/blue function as in 'What Color is Your Function'. Note that 'What Color is Your Function' is talking about whether or not the function is async/returns a callback, and that similar reasoning is needed esp. in Haskell for whether or not a function is pure. Here we are talking about whether a function possibly calls code provided by a user, eg code 'outside the module boundary' if theDAO is considered a 'module' (here, a trust/security boundary, eg we assume that everything inside the module boundary is correct and non-malicious, and anything outside may be incorrect and/or malicious).

So this adds evidence to the proposition that Oot should provide tools for easily labeling and tracing such things, even if the set of 'such things' is defined by an external framework rather than Oot.

---

list of ETH bugs:

https://blog.ethereum.org/2016/06/19/thinking-smart-contract-security/

in my view the way to deal with these is not (primarily) to change the EVM bytecode, but instead of have an awesome HLL like Oot that allows the creation of frameworks that provide more safety to the programmer.

Daian also says in a comment on the above post "What this implies is that the attack in the DAO goes beyond a simple exploit in the DAO's contract code itself, as some have been suggesting, and is actually a result of deeply flawed language constructs in Solidity."

---

a blog post on the Eth language Solidity:

" Some misfeatures are:

    A good language for writing state machines would ensure that there are no states from which it is impossible to recover.
    A good language for writing state machines would make it painfully clear when state transitions can and cannot happen.
    A good language for maintaining state machines would provide features for upgrading the security of a live contract.
    A good language for writing secure code would make it clear that there are no implicit actions, that code executes plainly, as read." -- [2]

---

these Synereo guys claim they have a system of formally typechecking what they call 'social graces' which appear to be properties of smart contracts:

http://blog.synereo.com/2015/03/06/on-social-contracts-part-ii/

on the difference b/t Synereo and former work on business process modeling languages:

" created Mar '15 last reply Mar '15 6 replies 517 views 5 users 8 likes 4 links 3

EdEykholt? Mar '15

Great post. I'm excited to learn more. I'm familiar with sequence diagrams, but am just now becoming more familiar with techniques for formal process specification applicable for decentralized protocols. Is Synereo's language for social contracts essentially a domain-specific language that extends pi-calculus in a consistent way? Are existing process modeling languages like BPDM, BPEL, BPML, or XLang not expressive enough or not domain-specific enough to be a good fit to specify social contracts? mathemagician Mar '15 1

EdEykholt? - Thank you for this question! Great to see you here in this forum. There is a close connection between the language of social contracts and the languages used in business process modeling. BPML and BPEL essentially owe their origins to XLang which in turn owes its origins to the π-calculus. i know because i invented XLang and the whole field of using process calculi to model business processes. You can check that with the US Patent Office wink.

There are three improvements in the language of social contracts. The first is to introduce structure into names. How much structure? That's such an interesting question. i explored the limits of this in my papers with Matthias Radestock on the rho-calculus. (See: this paper2 for example.) In the language of social contracts we actually dial it back to something that supports some practical considerations while fitting the domain requirements. The requirements have to with supporting distribution in a logical and satisfying way and is closely related to the second improvement.

The next improvement is to use a variant of the applied π-calculus where the messages exchanged are essentially prolog terms. When used in combination with the name structure improvement you get a two-fold structure for the notion of channel. There's a more heavy weight channel, fully qualified name, and then there's a lighter weight channel in the form of a pattern. Thus, for example

for( msg <- n?( c )( work( topics( [ "LivelyGig?" : X ] ) ) ) { display( msg ) }

provides a way to search on the channel c in the network entered through node n for messages labeled with

work( topics( [ "LivelyGig?" : X ] ) )

This semantics gives a broad range of processes semantics not present in the process modeling languages you mentioned.

Working in concert is the use of the for-comprehension. This solves several problems we encountered when working on XLang while at the same time making the model match the revolution going on with using reactive design patterns for high data volume applications. The practical problem with the π-calculus is that it doesn't do fork-join patterns well. The business process modeling languages use band-aid solutions without getting to the core of the issue. Using monadic semantics and the for-comprehension you get a pleasant syntactic solution for expressing fork-join patterns, along with the correspondingly nice semantics, and some peace of mind that the semantics is natural and well understood by the community.

i hope that helps! mathemagician Mar '15

i forgot to mention two other important differences. One is that the business process modeling offerings never got to the place where there was a formalized relationship between them and a model-checking or theorem-proving mechanism. With social contracts and social graces we complete that picture. Of course, in principle, this should be possible for any of the offerings. They just didn't do it, to the best of my knowledge.

The other difference, however is key. The business process modeling languages were never intended to be reduced to deployed code. Or, the relationship between the model and the executing code was more tenuous. In Synereo, the APIs go through the contract language. So, the contract and the code coincide.

This is important, because without such a correlation between contract and implementation you've got no way to guarantee conformance either to the contract or to the logical requirements expressed in the property language, e.g. Synereo's social graces. Closing this gap gives strong assurances about compliance to the contract. " -- [3]

---

" A purely functional language with a rich type system is needed. If we can't have that right now, All calls that send to untrusted address should have a gas limit Balances should be reduced before a send, not after one Events should probably have a Log prepended to their name. The splitDAO function should be mutexed and keep permanent track of the status of each possible splitter, not just through token tracking. "

-- http://vessenes.com/deconstructing-thedao-attack-a-brief-code-tour/

---

willtim 1 day ago

Modelling financial contracts in an imperative event-driven paradigm just seems like an accident waiting to happen.

EDIT: To the downvoters, if you disagree, I would very much like to understand why, please reply with a comment.

EDIT2: My position is that it is very difficult to reason about correctness and maintain invariants in a highly imperative setting. IMHO, it would be more desirable to use a declarative, or functional language. There are many successful commercial applications of functional programming to financial contracts, e.g. Lexifi, which is based on a subset of OCaml and various in-house solutions developed by banks. Using a functional programming language would also mean the code is far more amenable to formal methods and static verification. One new startup I was very impressed with, aestheticintegration.com, has had success rewriting financial algorithms in a functional programming language in order to prove and verify numerous correctness properties about them. It is a huge shame that folk do not reach straight for the functional programming toolbox when faced with these types of problems.

pron 1 day ago

I think you are placing far too much emphasis on language, especially as so far there's little evidence that some programming approaches yield less logical errors than others. I often see a similar sentiment expressed by people who are familiar with functional programming but unfamiliar with software verification, and may be unaware that nearly all verified software in the industry is written in imperative languages. I know many FP people like to believe that the local guarantees made by their chosen languages end up making their programs more globally correct; it may well be true that some languages make some errors easier to spot for humans (although we have little evidence to suggest that this is indeed the case of FP). However, as far as formal verification is concerned, there is very little overlap between verified software and FP.

Ensuring correctness -- i.e. conformance to a specification -- is, in general, a task that requires effort -- by man and/or machine -- proportional only to the complexity of the algorithm verified (i.e., the number of states reachable by a TM implementing it) and almost not at all to some linguistic properties. That is not to say that languages cannot prevent local errors that may be catastrophic, but the difference between the best of languages and the worst of languages when it comes to verifying spec-compliance is not that big.

> Using a functional programming language would also mean the code is far more amenable to formal methods and static verification

That is not true. If anything, imperative languages have better formal verification tools than functional ones. And besides, for global program "correctness" properties, the choice of a language more or less amenable to formal reasoning may make a difference that is surprisingly small.

...

In fact, while the difference between programming language in terms of general amenability to formal methods is not great, there are certainly large differences in amenability to model checking. This is why a language like SCADE (based on Esterel and the FRP-ish Lustre) is a fairly widely used tool in aviation software. If anything, a synchronous language like Esterel or the modern Céu[2] are a better choice if you want your verification to be as automatic as possible and run in a resource-constrained environment (that's killing two birds with one stone).

> As far as Europe is concerned, FP does appear to be the future of formal verification.

Even if you look at INRIA, the most European of institutions and the birthplace of Coq, you'll see that they dedicate significant verification research to other approaches[3]. At Max Planck, FP is a clear minority[4].

And if you look at the academic community at large without artificially restricting it to Europe (which certainly has a linguistic bias), you'll see that the verification community is certainly not betting on FP (although they are certainly exploring it). Don't get me wrong: FP and linguistic approaches is certainly one avenue among several showing promise in verification. But it is downright false to say that this approach is recognized as "the future of verification".

[1]: https://verificationinstitute.org/wp-content/uploads/sites/2...

[2]: http://www.ceu-lang.org/

[3]: http://www.inria.fr/en/teams/veridis

[4]: http://plv.mpi-sws.org/

...

> The advantage of the dependant-type approaches like Coq and Agda, is that the language of proof and implementation is now one of the same,

Two things. First, you can implement a system in Isabelle, too. Second, that advantage -- if it is one -- is rather theoretical at this point. Dependently typed languages have never been used outside of the lab, and have never been used in a large project. The approach, BTW, has plenty of disadvantages. First, the languages are very hard to learn, and require some very exotic, obscure math; second, some very important properties like time and space complexity -- that are often just as essential as logical correctness for those application where correctness matters most -- are hard to express, and there's no consensus yet on how to best reason about them. In short, dependent type approaches may one day be useful, but in general, we're not sure exactly how to use them yet.

> a total functional program can serve as both an executable specification and a logic with which one can derive proofs from

That is absolutely true, but this has some very severe disadvantages as well.

...

I have no doubt. But you should be aware that FP approaches to verification are just some of the many avenues in verification research these days, and are not generally accepted to be the most promising ones. In addition, unlike other approaches, they have pretty much never been put to the test outside the lab. Finally, SMT solvers are successfully used to verify Java programs (with JML specifications), and in the research world, Microsoft's Dafny[1] -- an imperative, non-functional (I think) language -- is a very popular choice in verification challenges (alongside tools like KIV[2] and Why3[3]). They also, I think, serve as the core proof method of SPARK Ada, a heavy duty verifiable language, with a good track record over many years in the industry.

[1]: http://research.microsoft.com/en-us/projects/dafny/

[2]: http://www.isse.uni-augsburg.de/en/software/kiv/

[3]: http://why3.lri.fr/

[4]

...

pron 6 hours ago

Oh, you are right that finite-state machines make automated verification easier (assuming that by Turing machine you meant Turing complete). However, some people are under the impression that other sub-Turing-complete languages (in particular, total functional programs) are easier to verify than programs in Turing-complete languages. This is false. The only class of languages that are practically "easy" to verify are finite state machines (well, if you call being PSPACE-complete easy; even that is exponential in the program's size!). This is easy to prove (in fact, it is a simple corrolary of the time hierarchy theorem and its proof). In particular, it is trivial to show that the problem of verifying a program in a total language is harder than any problem with a computable complexity bound, i.e. it's complexity is non-computable, i.e. it has "busy beaver" complexity[1]. I'm giving a talk on this precise subject next month at Curry On (http://curry-on.org/2016/sessions/why-writing-correct-softwa...)

[1]: The difference, therefore, between verification of Turing-complete programs and total programs is that the cost of verifying the former in the general case is infinite, while the cost of the other grows like some function that is larger than any function we can ever compute. From the perspective of computing power, both are equally beyond reach.

devit 1 day ago

The actual issue is the fact that sending money to someone can result in untrusted code running in the middle of your code execution and even reentering it seems absurd.

Sending should always succeed immediately and if anything needs to be automatically triggered in response, the trigger should be executed asynchronously.

A great way to immediately see the problem is, for anyone with Rust experience, to think of this as a function taking an &mut self being somehow reentered without that &mut self being passed out by the function itself.

johnbender 1 day ago

I would go further.

Given the sums of money involved I think it might also be worthwhile to have a formal semantics and a logic for proving safety properties of these blockchain programs (beyond type safety).

Not every application would require that kind of rigour but if the participation and value of a given currency/contract/program is determined largely by trust then it seems natural to want more serious guarantees.

mietek 19 hours ago

Note that a type system, if done properly, is simply another name for a logic for proving properties of programs.

Examples:

Agda (http://wiki.portal.chalmers.se/agda/pmwiki.php)
Coq (https://coq.inria.fr)
Idris (http://www.idris-lang.org)

willtim 1 day ago

I agree. I covered this only briefly under 'formal methods'. My point was that such formal semantics and proofs are far more easily obtained starting from a functional language.

-- https://news.ycombinator.com/item?id=11928376

---

jacquesm 1 day ago

This code is very bad, without going into an exhaustive enumeration, case sensitive function names, variables with unclear scope all over the place and so on.

That it's imperative code is something that I don't think is damning by itself but all the side-effects (including side effects based on a single bit in the name of a function) really do warrant the 'accident waiting to happen'.

---

    ```
        Transfer(msg.sender, 0, balances[msg.sender]);
    ```

Should have looked like this:

    ```
        // postcondition: balances[msg.sender] == 0
        Transfer(msg.sender, 0, balances[msg.sender]) :: Action<Transfer>;

    // Compiler result:
    // # Error 1: line XX expected type Action<Transfer> but instead got type Transfer
    // # Error 2: line XX violates postcondition, expected balances[msg.sender] == 0, got balances[msg.sender] != 0
    ```

And the whole function 'splitDao' should have a type annotation that completely captures the possible actions it might encompass, and pre- and postconditions that at the very least constrain the result of the function to not corrupt the accounting of the DAO (i.e. it should still have as many tokens as it believes it has).

---

" We can categorize the list by categories of bugs:

    Variable/function naming mixups: FirePonzi, Rubixi
    Public data that should not have been public: the public RNG seed casino, cheatable RPS
    Re-entrancy (A calling B calling A): the DAO, Maker’s ETH-backed token
    Sends failing due to 2300 gas limit: King of the Ether
    Arrays/loops and gas limits: Governmental
    Much more subtle game-theoretic weaknesses where at the limit people even debate whether or not they’re bugs: the DAO"

" The gas limit, however, is not going away; hence, the only solutions there are likely to be inside of the development environment itself. Compilers should throw a warning if a contract does not provably consume less than 2300 gas if called with no data; they should also throw a warning if a function does not provably terminate within a safe amount of gas. Variable names might be colored (eg. RGB based on the first three bytes of the hash of the name), or perhaps a heuristic warning might be given if two variable names are too close to each other.

Additionally, there are coding patterns that are more dangerous than others, and while they should not be banned, they should be clearly highlighted, requiring developers to justify their use of them. A particularly involved example is as follows. There are two types of call operations that are clearly safe. The first is a send that contains 2300 gas (provided we accept the norm that it is the recipient’s responsibility not to consume more than 2300 gas in the case of empty data). The second is a call to a contract that you trust and that is itself already determined to be safe (note that this definition bans re-entrancy as you would then have to prove A is safe before proving A is safe).

As it turns out, very many contracts can be covered by this definition. However, not all of them can; an exception is the idea of a “general purpose decentralized exchange” contract where anyone can place orders offering to trade a given amount of asset A for a given amount of asset B, where A and B are arbitrary ERC20-compatible tokens. One could make a special-purpose contract just for a few assets, and thereby fall under the “trusted callee” exemption, but having a generic one seems like a very valuable idea. But in that case, the exchange would need to call transfer and transferFrom of unknown contracts and, yes, give them enough gas to run and possibly make a re-entrant call to try to exploit the exchange. In this case, the compiler may want to throw a clear warning unless a “mutex lock” is used preventing the contract from being accessed again during those calls.

A third category of solutions is defense in depth. One example, to prevent losses (but not thefts) is to encourage all contracts that are not intended to be permanent to have an expiry date, after which the owner can take arbitrary actions on behalf of the contract; this way, losses would be possible only if (i) the contract screws up, and simultaneously (ii) the owner is missing or dishonest. Trusted multisig “owners” may emerge to mitigate (ii). Thefts could be mitigated by adding waiting periods. The DAO issue was greatly mitigated in scope precisely because the child DAO was locked down for 28 days. A proposed feature in the MakerDAO? is to create a delay before any governance change becomes active, allowing token holders unhappy with the change time to sell their tokens; this is also a good approach.

Formal verification can be layered on top. One simple use case is as a way of proving termination, greatly mitigating gas-related issues. Another use case is proving specific properties – for example, “if all participants collude, they can get their money out in all cases”, or “if you send your tokens A to this contract, you are guaranteed to either get the amount of token B that you want or be able to fully refund yourself”. Or “this contract fits into a restricted subset of Solidity that makes re-entrancy, gas issues and call stack issues impossible”. "

-- https://blog.ethereum.org/2016/06/19/thinking-smart-contract-security/

---

internet of code:

https://www.reddit.com/r/haskell/comments/3p2bfo/the_internet_of_code/

https://github.com/ipfs/apps/issues/6

http://www.haskellforall.com/2015/05/the-internet-of-code.html

http://www.haskellforall.com/2014/09/morte-intermediate-language-for-super.html

---

alan kay likes this:

http://www.rand.org/pubs/research_memoranda/RM5772.html

[5]

---

concolic testing: "performs symbolic execution, a classical technique that treats program variables as symbolic variables, along a concrete execution (testing on particular inputs) path. Symbolic execution is used in conjunction with an automated theorem prover or constraint solver based on constraint logic programming to generate new concrete inputs (test cases) with the aim of maximizing code coverage. Its main focus is finding bugs in real-world software" [6]

" An important reason for the rise of concolic testing (and more generally, symbolic-execution based analysis of programs) in the decade since it was introduced in 2005 is the dramatic improvement in the efficiency and expressive power of SMT Solvers. The key technical developments that lead to the rapid development of SMT solvers include combination of theories, lazy solving, DPLL(T) and the huge improvements in the speed of SAT solvers. SMT solvers that are particularly tuned for concolic testing include Z3, STP, Z3str2, and Boolector. "

---

SMT solvers:

https://en.wikipedia.org/wiki/Satisfiability_modulo_theories

---

"Game programmers and blockchain developers are already familiar with creating deterministic programs by avoiding sources of non-determinism such as:

    random number generators (without deterministic seeding)
    race conditions on threads (or avoiding threads altogether)
    the system clock
    uninitialized memory (in unsafe programming languages like C or C++)
    floating point arithmetic
    language features that are random (e.g. map iteration in Go)

note: they link to the same 'Gaffer' floating point determinism blog post that i've seen before: http://gafferongames.com/networking-for-game-programmers/floating-point-determinism/

---

elixir is moving towards prohibiting local mutations that extend outside of the current scope, even 'if' statement scope. [7]

---

possibly of some interest, i havent looked yet:

https://google.github.io/flatbuffers/

---

https://fsharpforfunandprofit.com/posts/is-your-language-unreasonable/

talks about predictability (ability to reason about code) as a language criteria. Interestingly, it echos that Clojure guy's point about how it's important that the language does NOT permit. It makes the additional point that NOT permiting things is hard to add in later versions of the language (because it would be very backwards-incompatible). It presents a list of criteria for predictability, and for each one, presents a code example showing how it can be annoying if your language lacks this criterion. The list is:

" How to make your language predictable:

    Variables should not be allowed to change their type. ((the example also covers unexpected long-range mutation, though))
    Objects containing the same values should be equal by default.
    Comparing objects of different types is a compile-time error.
    Objects must always be initialized to a valid state. Not doing so is a compile-time error.
    Once created, objects and collections must be immutable.
    No nulls allowed.
    Missing data or errors must be made explicit in the function signature."

Notes on downsides of these:

    Comparing objects of different types is a compile-time error.This makes it impossible to compare two different subclasses of the same class, which is often called for

    Objects must always be initialized to a valid state. Not doing so is a compile-time error.This makes it impossible to create a set of objects with circular dependencies.

imo there is a safety/extensibility tradeoff here. Another example of this tradeoff: if you declare an attribute of a class, and then later want to replace it with an implicit setter/getter (like Python properties), then if this is possible, then the class user has no guarantees on the behavior of class attributes (eg x.a = 1 does not guarantee that x.a == 1 will be True, because eg the setter for a might just discard its input and do nothing).

here's what i think i will choose for Oot:

    Variables should not be allowed to change their type.yes, have static typing

    ((the example also covers unexpected long-range mutation, though))yes, disallow long-range mutation unless the & sigil is used.

    Objects containing the same values should be equal by default.yes, this is a good default. (the criterion is about how eg Equals and GetHashCode? work; in some OOP languages, if these are not implemented, then the object just cannot support equality comparisons; the proposal is that all new classes should by default support these)

    Comparing objects of different types is a compile-time error.no, i want subclassing.

    Objects must always be initialized to a valid state. Not doing so is a compile-time error.instead of simply requiring this, have a built-in framework for 'initialized' vs 'uninitialized' objects.

    Once created, objects and collections must be immutable.by default, yes, but with the & sigil, can have mutable ones.

    No nulls allowed.yes. this criterion is about Maybe/Option types.

    Missing data or errors must be made explicit in the function signature.yes.

    I could go on, with snippets demonstrating the misuse of globals, side-effects, casting, and so onside-effects are in the inferred type signature and demand a & sigil except for masked domains. We have semiglobals (dynamic scoping) instead of globals. "

---

https://github.com/WebOfTrustInfo/ID2020DesignWorkshop/blob/master/topics-and-advance-readings/DexPredicatesForSmarterSigs.md section 'Temporary Delegation' has the interesting idea of what i call a 'monotonically semi-deterministic expression'; it can contain the function 'is_before(time)'; is_before(time) returns TRUE if 'time' is before the current time when the expression is being evaluated, and FALSE otherwise. So any time after is_before() returns TRUE, is_before will also return TRUE. So as long as the 'time' argument is before the current time at the time when the expression is constructed, the expression will seem to be deterministic if evaluated afterwards.

---

https://github.com/WebOfTrustInfo/ID2020DesignWorkshop/blob/master/topics-and-advance-readings/DexPredicatesForSmarterSigs.md contains an example which reminded me of something unrelated:

" (and (sig_valid <master_pubkey> (car (car (cdr argm))) (SHA256 (cdr (car (cdr argm))))) (eval ((cdr (car (cdr argm)))) (cons argm (cdr (cdr argm)))))

That expression is rather hard to read with all the car's and cdr's used on argm directly; here's it with symbolic names instead:

(and (sig_valid <master_pubkey> <binding_sig> (SHA256 <delegated_expr>) (eval <delegated_expr> (cons argm <sig_expr>)) "

this reminds me that one of the main functions of an HLL is to allow you to map names to parts of a data structure. This is similar to the function of keeping track of variable names (which maps names to locations in memory), but it's different in that this map's codomain is not a variable namespace, but rather the shape of a particular data structure. But, as Urbit reminds us, these can be generalized to the same thing (the Urbit 'subject' is the state, and the same operations manipulate parts of the subject and manipulate parts of particular data structures within it).

to reiterate/summarize:

one of the main functions of an HLL is to provide a mapping of names to variable value storage
another is to provide a mapping of names to attribute storage within a composite data structure
if the variable context (state) is reified as in Urbit, then we see that the same operations that address parts of the variable context can be used to address parts of composite data structures ---

https://fsharpforfunandprofit.com/posts/correctness-type-checking/ talks about nice type system features in F#

it's lightweight to define new types, allowing you to use specialized types for various things, eg "type EmailAddress? = EmailAddress? of string" ("In practice, we would also hide the constructor of the EmailAddress? type as well, to ensure that only valid values could be created in the first place")
F# compiler knows about printf format strings and analyzes them to give compile time errors for eg printf "a string %s" 2 , printf "a string %s" (missing param), printf "a string %s" "he" "lo"
- (am i understanding this correctly? a hardcoded special case for format strings? if so, i guess we would use this with Elixir-style custom sigils, eg a 'format string' sigil, something like ~f""; unless we decide that we like the new Python format syntax better: https://docs.python.org/2/library/string.html#format-examples)
units of measure (we do this with the 'U' shortcut, which i guess adds a type attribute?)
- F# makes a distinction between ordinary numbers which are a type error to mix with unit-ed numbers, and numbers with a unit of 'wildcard', which behave like unitless numbers (ie take on the units of the numbers they are mixed with). I think we can just have unitless numbers.
- F# deals with numbers with units like cm/meter, which, when multiplied by something with units 'meter' will return something of units 'cm'. I guess we can do this just by having eg 100Ucm / 1Umeter.

todo read the rest

---

F# property/getter syntax:

public class NaiveShoppingCart?<TItem> { private List<TItem> items; private decimal paidAmount;

   public NaiveShoppingCart()
   {
      this.items = new List<TItem>();
      this.paidAmount = 0;
   }

   /// Is cart paid for?
   public bool IsPaidFor { get { return this.paidAmount > 0; } }

...

---

so what don't we allow in Oot (that makes programs more 'predictable' ie easier to reason about)?

covert long-range side-effects covert long-range mutation covert blocking io covert nulls variables changing their type

---

"Coconut" looks great!

Some comments about it from HN:

" hcarvalhoalves 1 day ago

This is cool, but you can go pretty far w/ FP idioms in Python without requiring a DSL/transpiler:

Toolz (http://toolz.readthedocs.io/en/latest/) provides the same primitives from Clojure (including partial functions, compose, juxt, etc)
Pysistence (https://pypi.python.org/pypi/pysistence/) provides immutable data structs
For parallel map you can use https://pypi.python.org/pypi/python-pmap/1.0.2
TCO is achievable w/ a decorator regardless of AST manipulation (like Clojure's `loop/recur` construct)

The only thing left is pattern matching and more powerful destructuring (Python already has limited support for it), I guess.

reply "

---

python, using generator expressions:

    sum_of_squares = sum(x*x for x in arr)

numlocked 1 day ago

Worth noting that map() can be parallelized whereas a list comprehension can't necessarily (since it is an explicit loop). The multiprocessing module allows trivial map parallelization, but can't work on list comprehensions.

It's more than just stylistic.

fovc 1 day ago

map() can only be parallelized if the function has no side effects. If there are no side effects, list comprehensions can be parallelized just as well

S4M 1 day ago

That example works only because the function sum is already defined in Python. If you wanted to do something less common than summing up elements you would have to either use reduce or implement a for loop.

Orangeair 1 day ago

In Python 3, reduce was intentionally moved into the functools library because it was argued that its two biggest use cases by far were sum and product, which were both added as builtins. In my experience, this has very much been the case. Reduce is still there if you need it, and isn't any more verbose. The only thing that is a little bit more gross about this example is the lambda syntax; I would argue that even that is a moot point, however, since Python supports first-class functions, so you can always just write your complicated reduce function out and then plug it in.

zardeh 1 day ago

True, but I've used python a lot, and I've used reduce maybe...twice? (well, twice that I can find on my github at least)

---

dang 11 minutes ago

I've been writing JS a long long time and my strategy has been never to learn the intricacies of 'this'—or the other bad neighborhoods of that language, but especially 'this'. I just avoid those neighborhoods. I write functions at the top level, keep all the signatures explicit, and enjoy the things the language does well.

Once every couple years or so I need to do something that requires me to step foot into understanding a little of 'this'. If Plan A (find a way to avoid it) fails, I go to Plan B: relearn the minimum necessary and forget it as soon as possible.

---

notes on http://atastypixel.com/blog/four-common-mistakes-in-audio-development/

he doesnt use the phrase 'soft realtime' but afaict that's what he's talking about, although i don't know what i'm talking about here so i could be wrong.

afaict the 'four common mistakes' all boil down to: "don't block the audio thread". In particular:

don't request locks
don't use Objective-C/Swift (Like [myInstance doAThing] or myInstance.something)
- b/c the Objective-C/Swift implementations lock while message sending, while accessing a property, or retaining
- see the article for details, section "Objective-C and Swift hold locks as part of their normal operations" and "So, what’s to be done?")
- but you can probably declare variables __unsafe_unretained, and then access them as ordinary C structs from C functions within the @implementation block
don't allocate memory (can take a very long time; also, malloc uses a lock)
don't do I/O

note on priority inversion and locks: if you request a lock on the audio thread and the lock requested is being held by another thread , the audio thread will block until the other thread reliquishes the lock. You might think you could get away with that as long as the other thread only holds the lock for a very short time, by only doing a few quick operations in the lock. But the other thread might be pre-empted by a third thread while it is in the lock, so actually the lock may be held for a long time even if the other thread isn't doing much inside the lock. This is called 'priority inversion' because this is a way in which the third thread can (indirectly) hold up the high-priority audio thread even if the third thread is of lower priority (in the scheduler) than the audio thread. My note: in order for priority inversion to occur, the other thread would have to be a lower scheduler priority than the audio thread; if the other thread is the same priority as the audio thread than afaict you're safe from this particular problem.

low-level alternatives to locks:

libkern/OSAtomic.h: OSAtomicEnqueue? and OSAtomicDequeue?, OSAtomicAdd?32Barrier and OSMemoryBarrier?
"..use try locks (like pthread_mutex_trylock), as long as you have a decent idea what you’ll do if you don’t get the lock."
"on all modern processors, you can safety assign a value to a int, double, float, bool, BOOL or pointer variable on one thread, and read it on a different thread without worrying about tearing, where only a portion of the value has been assigned by the time you read it... byte, halfword and word-length assignment is atomic...as long as the variable is naturally aligned — which it will be, if it’s an Objective-C instance variable or in an un-packed struct...Note that this doesn’t necessarily apply to variables of other types; if you’re on a 32-bit processor and you assign a uint64_t variable, you could get into trouble"

related libraries:

" What about libdispatch, and using blocks?

Unfortunately, these are off-limits, too. While you can safely call a block on the audio thread, as long as you don’t retain or release it there, creating a block on the audio thread causes some memory allocation as well as some object retains, both of which will hold locks. But I have good news on that front; if you’re impatient, skip down to the bit about AEMessageQueue?. "

"TPCircularBuffer? is a widely-used circular buffer library... It’s built right into The Amazing Audio Engine 2, as AECircularBuffer?.... It also lets you read and write AudioBufferLists?, both interleaved and non-interleaved, and carries AudioTimestamp? values too, all of which makes it convenient for use with Core Audio. "

"AEManagedValue? from The Amazing Audio Engine 2 provides a pointer variable which is carefully managed so that assignments are atomic and release occurs only once the audio thread has finished with the value."

" AEArray, also from The Amazing Audio Engine 2, builds upon AEManagedValue? to implement a map between an NSArray and a C array which you can access safely on the audio thread. You can either access the Objective-C instances directly on the audio thread, or you can provide a block which will map between those Objective-C objects and a C structure."

"AEMessageQueue?, again from The Amazing Audio Engine 2, lets you schedule blocks to be performed on the audio thread...and in the other direction allows you to safely schedule a target/selector on the main thread...This works a bit like libdispatch, but is completely audio thread safe."

"how do you know if you have a problem?"

 Realtime Watchdog
 "(also now built right into The Amazing Audio Engine 2..."

"It won’t catch everything, and it won’t catch anything in Apple’s own system code, but it’ll catch some locks, some memory allocation, all Objective-C use (but not Swift), all object retains, and some common IO tasks, in your code and that of any static libraries you’re using. "

" If you’re seeing crackling and glitching and you’ve taken care of the above, then you might want to look at optimising your code; in particular, replacing any scalar operations with vector ones, using something like the Accelerate framework. "

post also contains "A survey of popular audio engine libraries and their audio thread safety"

---

some advice someone gave:

" Avoid using language extensions and libraries that do not play well with your IDE. The impact they will have on your productivity will far outweigh the small benefit of easier configuration or saving a few keystrokes with more terse syntax.

Using ServiceLocator? is an example of design that leads to poor integration with most IDEs:

ServiceLocator?.get('serviceName')

Another way to keep the “integrated” part of your IDE relevant is to avoid magic code. Most languages will provide ways for you to write more dynamic code. Abusing these features such as by using magic strings, magic array indexes and custom template language features will lead to a more disconnected codebase. Generally any features which only a human will know the meaning of will lead you down this road, and it’s a hard road to come back from, because if your IDE doesn’t understand the code, any refactoring features it has are going to be useless when you want to move to a more static architecture. "

we need to keep this in mind when thinking about Oot metaprogramming and component architecture

---

my notes on this guy's advice for readable code:

http://chrismm.com/blog/writing-good-code-reduce-the-cognitive-load/

don't be clever
divide and conquer
- eg create more functions
- eg Storing the result of long conditionals into a variable or two
- eg Programming languages and libraries often come with their issues, and abstracting them away can help your code mind its own business
- eg Single responsibility principal
- eg make your code unit testable
try to have each part as focused as possible, affecting only local state, without mixing in irrelevant issues, and without side-effects if at all possible
avoid language extensions and libraries that don't play well with your IDE
avoid programming techniques that do control flow via string names for things, because your IDE can't follow this
"Once you’ve agreed on an overall architectural structure for your project, make it obvious where the main elements are located. Using MVC? Place models, views and controllers in their own folders, not three folders deep or spread across several different places."
"Try to use fewer libraries by choosing the ones that cover as many of your needs as possible"
don't use very new technologies, some other devs might not know them yet
choose descriptive names
document the why
keep number of conditional branches low (cyclomatic complexity)
recommends Code Complete

---

time (wmctrl -d

real 0m0.020s

perl -lane 'print $F[8]')

time (wmctrl -d

awk '{print $9}')

real 0m0.005s

for a GUI script this may be important...

although once i got:

time (wmctrl -d

awk '{print $9}')

real 0m0.028s

and

time (wmctrl -d

perl -lane 'print $F[8]')

real 0m0.006s

---

" ... I agree, but there's already so much stuff that doesn't belong in kernel space inside Linux and FreeBSD?, that this doesn't make it any worse. We will hopefully see the rise of something based on seL4 (microkernel) or Barrelfish's multikernel design (one kernel per core, no shared memory) "

---

" FreeBSD? also has Netmap and DTrace out of the box. They will also get TLS support in sendfile(2) as soon as the patches from Netflix land in HEAD. "

---

ppl like Solaris and FreeBSD?'s Zones and Jails eg [8] eg [9]

---

a few ppl dislike Linux's epoll and prefer either Solaris's completion ports, NT's IOCP, or BSD's kqueue:

" Of course, there's the larger issue of Linux being insular, with a tendency to reinvent the wheel (epoll vs. kevent/kqueue being a nice example) rather than looking at what the state of the art is elsewhere and adopting that. You just have to look at containerisation: Solaris and FreeBSD? have long had this in the form of Zones and Jails[1], but containerisation on Linux is largely an independent effort that didn't look to learn lessons from those efforts or adopt them. "

smegel 13 hours ago

parent

flag

on: BSD vs. Linux (2005)

BSD has a wonderful, unified events system. That incorporates blocking disk IO. Linux has epoll.

https://www.nginx.com/blog/why-netflix-chose-nginx-as-the-he... https://www.nginx.com/blog/why-netflix-chose-nginx-as-the-heart-of-its-cdn/

PeCaN? 11 hours ago

BSD and Solaris (which also has kqueue, and something else IIRC) got this really right while Linux got this really wrong.

I still prefer NT's IOCP, but kqueue isn't bad. epoll… is what happens when you get someone who's never done asynchronous I/O to design a system for doing asynchronous I/O.

aseipp 46 minutes ago

Solaris has its own form of completion ports too, I believe. https://web.archive.org/web/20110719052845/http://developers... https://web.archive.org/web/20110719052845/http://developers.sun.com/solaris/articles/event_completion.html

NT's IOCP is good, sensible model overall having used it some recently. It's mildly put off by some "gotchas" (like async calls occasionally returning synchronously if there's nothing else on the queue, so you have to be careful with send, recv, etc), but the actual design is good. Thread pools being a convenient, native API in Vista+ is also a bonus.

---

" DataKit?

DataKit? is a toolkit to coordinate processes with a git-compatible filesystem interface. It revisits the UNIX pipeline concept and the Plan9 9P protocol, but with a modern twist: streams of tree-structured data instead of raw text. DataKit? lets you define complex workflows between loosely coupled processes using something as simple as shell scripts interacting with a version ttcontrolled file-system.

DataKit? is a rethinking of application architecture around data flows, bringing back the wisdom of Plan 9s everything is a file, in the git era where everything is a versioned file. Since we are making use of DataKit? and 9P heavily in Docker for Mac and Windows, we are also open sourcing go-p9p, a modern, performant 9P library for Go. "

kevinmgranger 1 day ago

docker's go-9p now makes for the 3rd implementation of 9p in go:

docker/go-9p https://github.com/docker/go-p9p

rminnich/ninep: https://github.com/rminnich/ninep

rminnich/go9p: https://github.com/rminnich/go9p

There's also the Andrey Mirtchovski and Latchesar Ionkov implementation of go9p, but all I can find is a dead Google Code link from here: http://9p.cat-v.org/implementations

justincormack 22 hours ago

We did try the other implementations first, but had a lot of issues doing what we wanted with them.

http://vessenes.com/ethereum-contracts-are-going-to-be-candy-for-hackers/

---

Furthermore, just having had a quick scan over the language documentation, it looks to me like a bog-standard imperative mutable language. One that is very young, and with few if any features designed for being used in a high-security environment. It appears to be based on raw event-based programming, a style of programming very easy to mess up and hard to declare and preserve invariants in. It looks like a very dangerous programming language to be trying to write financial contracts in. At least it's not dynamically typed, does seem to avoid excessive coercion, and should be memory safe; it could certainly be worse. But it could be better, too.

-- https://news.ycombinator.com/item?id=11726734 (about Solidity)

---

could have deterministic mapping of arbitrary UI inputs to controls given:

whether it is multiple choice (exclusive or nonexclusive (radio circles or checkboxes), word input, etc
occurrency frequency, co-occurence frequency, approximate sequence frequency (eg do people tend to push this one shortly after that one? how frequent is that pattern as a fraction of all 'this ones' and of all 'that ones'?), hidden markov frequencies (eg inferred 'modes' of the application, eg in a pilot sim there might be 'combat mode' and 'travel mode' and 'landing mode' etc)
what the user needs to be looking at when they press it; whether it requires mouse navigation in addition to pushing a button or not
need for latency, precision
for combo (multikey) inputs, how 'easy' is the combo physically (note: if the user probably already has their thumb on one of the combo keys, then pushing that key as part of the combo is 'easier' than pushing a key under another finger. So you see that all of the above questions have correlates in both the specification of the inputs and of the program. Note, however, that the program control statistics can be collected from usage data (except for demand for latency and precision), whereas the easiness of inputs probably has to be specified (or collected from a controlled 'game')

---

FST generator

http://imatix-legacy.github.io/libero/index.htm

https://github.com/imatix-legacy